HOL/Makefile: now test depends upon SUBST_FILES
HOL/Makefile/SUBST_FILES: changed some filenames to upper case
HOL/Makefile: now executes ex/ROOT.ML after Subst/ROOT.ML
(* 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