ex/puzzle.thy
author nipkow
Tue, 16 Aug 1994 09:57:51 +0200
changeset 104 a0e6613dfbee
parent 0 7949f97df77a
permissions -rw-r--r--
allow long_id for reference to type in primrec. Doesn't work yet, though, because of problems with the autoloader.

(*  Title: 	HOL/ex/puzzle.thy
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1993 TU Muenchen

An question from "Bundeswettbewerb Mathematik"
*)

Puzzle = Nat +
consts f :: "nat => nat"
rules  f_ax "f(f(n)) < f(Suc(n))"
end