# HG changeset patch
# User nipkow
# Date 942923559 -3600
# Node ID 2855e262129ccfd3a548b454e8a38ef45c6d843a
# Parent  9a400ba634b8c8b875d91aef7489823bf944fb25
Streamlined it a bit more.

diff -r 9a400ba634b8 -r 2855e262129c src/HOL/ex/Puzzle.ML
--- 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)";