tuned induct syntax;
authorwenzelm
Sat Nov 19 14:21:01 2005 +0100 (2005-11-19)
changeset 18204c3caf13f621d
parent 18203 9bd26bda96ef
child 18205 744803a2d5a5
tuned induct syntax;
src/HOL/Isar_examples/Puzzle.thy
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Sat Nov 19 14:21:00 2005 +0100
     1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Sat Nov 19 14:21:01 2005 +0100
     1.3 @@ -16,13 +16,12 @@
     1.4  *}
     1.5  
     1.6  theorem
     1.7 -  fixes n :: nat
     1.8    assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
     1.9    shows "f n = n"
    1.10  proof (rule order_antisym)
    1.11    {
    1.12      fix n show "n \<le> f n"
    1.13 -    proof (induct k \<equiv> "f n" rule: less_induct fixing: n)
    1.14 +    proof (induct k \<equiv> "f n" fixing: n rule: less_induct)
    1.15        case (less k n)
    1.16        then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
    1.17        show "n \<le> f n"