# HG changeset patch
# User wenzelm
# Date 1014998388 -3600
# Node ID 80dec7322a8c7c175de93e40e7d5ac74ca363c17
# Parent  7ac0a7e306db34635e390490323e858b7630f91e
tuned;

diff -r 7ac0a7e306db -r 80dec7322a8c src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Fri Mar 01 16:24:43 2002 +0100
+++ b/src/HOL/Isar_examples/Puzzle.thy	Fri Mar 01 16:59:48 2002 +0100
@@ -24,8 +24,7 @@
   show ge: "!!n. n <= f n"
   proof -
     fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
-    proof (induct k
-        rule: nat_less_induct [rule_format])
+    proof (induct k rule: less_induct)
       fix k assume hyp: "!!m. m < k ==> PROP ?P m"
       fix n assume k_def: "k == f n"
       show "n <= k"