1.1 --- a/src/HOL/Integ/Bin.ML	Mon Jul 19 15:27:34 1999 +0200
     1.2 +++ b/src/HOL/Integ/Bin.ML	Mon Jul 19 15:29:01 1999 +0200
     1.3 @@ -386,8 +386,9 @@
     1.4  
     1.5  (** Less-than-or-equals (<=) **)
     1.6  
     1.7 -Goal "(number_of x <= (number_of y::int)) = (~ number_of y < (number_of x::int))";
     1.8 -by (simp_tac (simpset() addsimps [zle_def]) 1);
     1.9 +Goal "(number_of x <= (number_of y::int)) = \
    1.10 +\     (~ number_of y < (number_of x::int))";
    1.11 +by (rtac (linorder_not_less RS sym) 1);
    1.12  qed "le_number_of_eq_not_less"; 
    1.13  
    1.14  (*Delete the original rewrites, with their clumsy conditional expressions*)
    1.15 @@ -674,6 +675,10 @@
    1.16  
    1.17  Addsimps [nat_0_le, nat_le_0];
    1.18  
    1.19 +val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
    1.20 +by (rtac (major RS nat_0_le RS sym RS minor) 1);
    1.21 +qed "nonneg_eq_int"; 
    1.22 +
    1.23  Goal "#0 <= w ==> (nat w = m) = (w = int m)";
    1.24  by Auto_tac;
    1.25  qed "nat_eq_iff";
    1.26 @@ -702,39 +707,6 @@
    1.27  by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.28  qed "nat_2";
    1.29  
    1.30 -Goal "nat #3 = Suc 2";
    1.31 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.32 -qed "nat_3";
    1.33 -
    1.34 -Goal "nat #4 = Suc (Suc 2)";
    1.35 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.36 -qed "nat_4";
    1.37 -
    1.38 -Goal "nat #5 = Suc (Suc (Suc 2))";
    1.39 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.40 -qed "nat_5";
    1.41 -
    1.42 -Goal "nat #6 = Suc (Suc (Suc (Suc 2)))";
    1.43 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.44 -qed "nat_6";
    1.45 -
    1.46 -Goal "nat #7 = Suc (Suc (Suc (Suc (Suc 2))))";
    1.47 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.48 -qed "nat_7";
    1.49 -
    1.50 -Goal "nat #8 = Suc (Suc (Suc (Suc (Suc (Suc 2)))))";
    1.51 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.52 -qed "nat_8";
    1.53 -
    1.54 -Goal "nat #9 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 2))))))";
    1.55 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.56 -qed "nat_9";
    1.57 -
    1.58 -(*Users also don't want to see (nat 0), (nat 1), ...*)
    1.59 -Addsimps [nat_0, nat_1, nat_2, nat_3, nat_4, 
    1.60 -	  nat_5, nat_6, nat_7, nat_8, nat_9];
    1.61 -
    1.62 -
    1.63  Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
    1.64  by (case_tac "neg z" 1);
    1.65  by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));