src/HOL/Nat.ML
changeset 9870 2374ba026fc6
parent 9637 47d39a31eb2f
child 9969 4753185f1dd2
     1.1 --- a/src/HOL/Nat.ML	Tue Sep 05 21:06:01 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Sep 06 08:04:41 2000 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  qed "Least_Suc";
     1.5  
     1.6  val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
     1.7 -by (rtac less_induct 1);
     1.8 +by (rtac nat_less_induct 1);
     1.9  by (case_tac "n" 1);
    1.10  by (case_tac "nat" 2);
    1.11  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));