# HG changeset patch
# User paulson
# Date 942833786 -3600
# Node ID fead0dbf5b0a68c07a88c069a3c356e338359e1d
# Parent  bedd0beabbae81fd8b3e459fd2967e6250180125
tidied

diff -r bedd0beabbae -r fead0dbf5b0a src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Mon Nov 15 09:41:06 1999 +0100
+++ b/src/HOL/ex/Puzzle.ML	Wed Nov 17 11:16:26 1999 +0100
@@ -15,13 +15,10 @@
 by (rtac allI 1);
 by (rename_tac "i" 1);
 by (exhaust_tac "i" 1);
- by (Asm_simp_tac 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (dtac not_leE 1);
+ by Auto_tac;
 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() addIs [Suc_leI,le_less_trans]) 1);
 val lemma = result() RS spec RS mp;
 
 Goal "n <= f(n)";