1.1 --- a/src/HOL/ex/Puzzle.ML	Mon Nov 15 09:41:06 1999 +0100
     1.2 +++ b/src/HOL/ex/Puzzle.ML	Wed Nov 17 11:16:26 1999 +0100
     1.3 @@ -15,13 +15,10 @@
     1.4  by (rtac allI 1);
     1.5  by (rename_tac "i" 1);
     1.6  by (exhaust_tac "i" 1);
     1.7 - by (Asm_simp_tac 1);
     1.8 -by (rtac impI 1);
     1.9 -by (rtac classical 1);
    1.10 -by (dtac not_leE 1);
    1.11 + by Auto_tac;
    1.12  by (subgoal_tac "f(nat) <= f(f(nat))" 1);
    1.13   by (Blast_tac 2);
    1.14 -by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
    1.15 +by (blast_tac (claset() addIs [Suc_leI,le_less_trans]) 1);
    1.16  val lemma = result() RS spec RS mp;
    1.17  
    1.18  Goal "n <= f(n)";