# HG changeset patch # User nipkow # Date 942911419 -3600 # Node ID 9a400ba634b8c8b875d91aef7489823bf944fb25 # Parent 2823ce1753a5b93d2227e4fb31ffac417b8ec80f A small mod. diff -r 2823ce1753a5 -r 9a400ba634b8 src/HOL/ex/Puzzle.ML --- a/src/HOL/ex/Puzzle.ML Wed Nov 17 15:03:23 1999 +0100 +++ b/src/HOL/ex/Puzzle.ML Thu Nov 18 08:50:19 1999 +0100 @@ -15,10 +15,11 @@ by (rtac allI 1); by (rename_tac "i" 1); by (exhaust_tac "i" 1); - by Auto_tac; + 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() addIs [Suc_leI,le_less_trans]) 1); +by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1); val lemma = result() RS spec RS mp; Goal "n <= f(n)";