(* Title: HOL/ex/pl0.thy ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen Syntax of propositional logic formulae. *) PL0 = HOL + datatype 'a pl = false | var ('a) ("#_") | "->" ('a pl,'a pl) (infixr 90) end