# HG changeset patch
# User wenzelm
# Date 1132406461 -3600
# Node ID c3caf13f621d594f151b7bf04ca58b57aa08f211
# Parent  9bd26bda96efe40515e765734e991b33471ff7ba
tuned induct syntax;

diff -r 9bd26bda96ef -r c3caf13f621d src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Sat Nov 19 14:21:00 2005 +0100
+++ b/src/HOL/Isar_examples/Puzzle.thy	Sat Nov 19 14:21:01 2005 +0100
@@ -16,13 +16,12 @@
 *}
 
 theorem
-  fixes n :: nat
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
   shows "f n = n"
 proof (rule order_antisym)
   {
     fix n show "n \<le> f n"
-    proof (induct k \<equiv> "f n" rule: less_induct fixing: n)
+    proof (induct k \<equiv> "f n" fixing: n rule: less_induct)
       case (less k n)
       then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
       show "n \<le> f n"