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.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Syntax of propositional logic formulae.
*)
PL0 = HOL +
types 'a pl
arities pl :: (term)term
consts
false :: "'a pl"
"->" :: "['a pl,'a pl] => 'a pl" (infixr 90)
var :: "'a => 'a pl" ("#_")
end