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