Reorganized/optimized datatype definitions.
(* 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