src/HOL/Isar_examples/Puzzle.thy
 changeset 18193 54419506df9e parent 18191 ef29685acef0 child 18204 c3caf13f621d
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 16 17:50:35 2005 +0100
1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 16 19:34:19 2005 +0100
1.3 @@ -4,13 +4,15 @@
1.4  theory Puzzle imports Main begin
1.5
1.6  text_raw {*
1.7 - \footnote{A question from Bundeswettbewerb Mathematik''.  Original
1.8 - pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
1.9 - Tobias Nipkow.}
1.10 +  \footnote{A question from Bundeswettbewerb Mathematik''.  Original
1.11 +  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
1.12 +  Tobias Nipkow.}
1.13 +*}
1.14
1.15 - \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to 1.16 - \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
1.17 - $n$.  Demonstrate that $f$ is the identity.
1.18 +text {*
1.19 +  \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
1.20 +  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
1.21 +  Demonstrate that $f$ is the identity.
1.22  *}
1.23
1.24  theorem