A small mod.
1.1 --- a/src/HOL/ex/Puzzle.ML Wed Nov 17 15:03:23 1999 +0100
1.2 +++ b/src/HOL/ex/Puzzle.ML Thu Nov 18 08:50:19 1999 +0100
1.3 @@ -15,10 +15,11 @@
1.4 by (rtac allI 1);
1.5 by (rename_tac "i" 1);
1.6 by (exhaust_tac "i" 1);
1.7 - by Auto_tac;
1.8 + by (Asm_simp_tac 1);
1.9 +by (rtac impI 1);
1.10 by (subgoal_tac "f(nat) <= f(f(nat))" 1);
1.11 by (Blast_tac 2);
1.12 -by (blast_tac (claset() addIs [Suc_leI,le_less_trans]) 1);
1.13 +by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
1.14 val lemma = result() RS spec RS mp;
1.15
1.16 Goal "n <= f(n)";