1
(* Title: HOL/ex/puzzle.thy
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1993 TU Muenchen
5
6
An question from "Bundeswettbewerb Mathematik"
7
*)
8
9
Puzzle = Nat +
10
consts f :: nat => nat
11
rules f_ax "f(f(n)) < f(Suc(n))"
12
end