isabelle: src/HOL/ex/Puzzle.thy@0140ff702b23 (annotated)

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