isabelle: src/HOL/ex/Puzzle.thy@63c3d78df538 (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 +
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 969 diff changeset	10	consts f :: nat => nat
969 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