# HG changeset patch
# User paulson
# Date 1184598817 -7200
# Node ID 5440f9f5522c1377d85d70c83739bdf46b169b28
# Parent  f935b85fbb4c988dc4448fdd62be4e02d3ee184a
tidied using sledgehammer

diff -r f935b85fbb4c -r 5440f9f5522c src/HOL/ex/Puzzle.thy
--- a/src/HOL/ex/Puzzle.thy	Mon Jul 16 09:29:05 2007 +0200
+++ b/src/HOL/ex/Puzzle.thy	Mon Jul 16 17:13:37 2007 +0200
@@ -31,15 +31,10 @@
 lemma lemma1: "n <= f(n)"
 by (blast intro: lemma0)
 
-lemma lemma2: "f(n) < f(Suc(n))"
-by (blast intro: le_less_trans lemma1)
-
 lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
 apply (induct_tac "n")
- apply simp
-apply (rule impI)
-apply (erule le_SucE)
- apply (cut_tac n = n in lemma2, auto) 
+ apply simp 
+ apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le)
 done
 
 lemma f_id: "f(n) = n"