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

2222 a3fb552f10e3 Added Lagrang. Modified comment. nipkow parents: 1476 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
2222 a3fb552f10e3 Added Lagrang. Modified comment. nipkow parents: 1476 diff changeset	6	A question from "Bundeswettbewerb Mathematik"
969 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