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