diff -r d3d727449d7b -r fded09018308 ex/PL0.thy
--- a/ex/PL0.thy	Fri Jun 17 14:15:38 1994 +0200
+++ b/ex/PL0.thy	Fri Jun 17 14:16:50 1994 +0200
@@ -13,4 +13,6 @@
     false	:: "'a pl"
     "->"	:: "['a pl,'a pl] => 'a pl"	(infixr 90)
     var		:: "'a => 'a pl"		("#_")
+datatype
+    'a pl = false | var('a) | "op->" ('a pl,'a pl)
 end