(* 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)"
);