HOL/ROOT/HOL_dup_cs: removed as obsolete
HOL/ROOT: now passes "classical" to Classical_Fun
HOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
(* 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