changeset 8022 | 2855e262129c |
parent 8021 | 9a400ba634b8 |
child 8423 | 3c19160b6432 |
--- a/src/HOL/ex/Puzzle.ML Thu Nov 18 08:50:19 1999 +0100 +++ b/src/HOL/ex/Puzzle.ML Thu Nov 18 12:12:39 1999 +0100 @@ -16,10 +16,7 @@ by (rename_tac "i" 1); by (exhaust_tac "i" 1); by (Asm_simp_tac 1); -by (rtac impI 1); -by (subgoal_tac "f(nat) <= f(f(nat))" 1); - by (Blast_tac 2); -by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1); +by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1); val lemma = result() RS spec RS mp; Goal "n <= f(n)";