src/HOL/Isar_examples/Puzzle.thy
changeset 20503 503ac4c5ef91
parent 18204 c3caf13f621d
child 31758 3edd5f813f01
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  proof (rule order_antisym)
     1.5    {
     1.6      fix n show "n \<le> f n"
     1.7 -    proof (induct k \<equiv> "f n" fixing: n rule: less_induct)
     1.8 +    proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
     1.9        case (less k n)
    1.10        then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
    1.11        show "n \<le> f n"