isabelle: src/HOL/ex/Puzzle.thy@69b93ffc29ec (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	1	(* Title: HOL/ex/puzzle.thy
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	3	Author: Tobias Nipkow
969 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