--- 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