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