src/HOL/Nat.ML
changeset 6115 c70bce7deb0f
parent 6109 82b50115564c
child 6301 08245f5a436d
     1.1 --- a/src/HOL/Nat.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Jan 13 12:16:34 1999 +0100
     1.3 @@ -54,12 +54,6 @@
     1.4  qed "not_gr0";
     1.5  AddIffs [not_gr0];
     1.6  
     1.7 -(*Goal "m<n ==> 0 < n";
     1.8 -by (dtac gr_implies_not0 1);
     1.9 -by (Asm_full_simp_tac 1);
    1.10 -qed "gr_implies_gr0";
    1.11 -Addsimps [gr_implies_gr0];*)
    1.12 -
    1.13  qed_goalw "Least_Suc" thy [Least_nat_def]
    1.14   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.15   (fn _ => [