--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/pl0.ML	Tue Mar 22 08:28:31 1994 +0100
@@ -0,0 +1,12 @@
+(*  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)"
+);