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/pl0.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Inductive definition of propositional logic formulae.
*)
structure PL0 = DeclaredDatatype
(val base = PL0.thy
val data = "'a pl = false | var('a) | \"op->\"('a pl,'a pl)"
);