| changeset 14126 | 28824746d046 |
| parent 13116 | baabb0fd2ccf |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/ex/Puzzle.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/ex/Puzzle.thy Thu Jul 24 16:36:29 2003 +0200 @@ -12,7 +12,9 @@ consts f :: "nat => nat" -axioms f_ax [intro!]: "f(f(n)) < f(Suc(n))" +specification (f) + f_ax [intro!]: "f(f(n)) < f(Suc(n))" + by (rule exI [of _ id], simp) lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"