src/HOL/Nat.ML
changeset 6109 82b50115564c
parent 5983 79e301a6a51b
child 6115 c70bce7deb0f
     1.1 --- a/src/HOL/Nat.ML	Tue Jan 12 17:19:53 1999 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Jan 13 08:41:28 1999 +0100
     1.3 @@ -52,13 +52,13 @@
     1.4   by (etac swap 1);
     1.5   by (ALLGOALS Asm_full_simp_tac);
     1.6  qed "not_gr0";
     1.7 -Addsimps [not_gr0];
     1.8 +AddIffs [not_gr0];
     1.9  
    1.10 -Goal "m<n ==> 0 < n";
    1.11 +(*Goal "m<n ==> 0 < n";
    1.12  by (dtac gr_implies_not0 1);
    1.13  by (Asm_full_simp_tac 1);
    1.14  qed "gr_implies_gr0";
    1.15 -Addsimps [gr_implies_gr0];
    1.16 +Addsimps [gr_implies_gr0];*)
    1.17  
    1.18  qed_goalw "Least_Suc" thy [Least_nat_def]
    1.19   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"