src/HOL/ex/Puzzle.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8018 bedd0beabbae
child 13116 baabb0fd2ccf
permissions -rw-r--r--
hide many names from Datatype_Universe.

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

A question from "Bundeswettbewerb Mathematik"
*)

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