--- a/Nominal/Test.thy Tue Mar 02 12:28:07 2010 +0100
+++ b/Nominal/Test.thy Tue Mar 02 13:28:54 2010 +0100
@@ -68,12 +68,12 @@
text {* example type schemes *}
-(* does not work yet
-nominal_datatype t =
- Var "name"
+nominal_datatype t =
+ Var "name"
| Fun "t" "t"
-nominal_datatype tyS =
+(* does not work yet
+nominal_datatype tyS =
All xs::"name list" ty::"t_raw" bind xs in ty
*)
@@ -137,12 +137,12 @@
(* example 4 from Terms.thy *)
-(* does not work yet
+
nominal_datatype trm4 =
Vr4 "name"
| Ap4 "trm4" "trm4 list"
| Lm4 x::"name" t::"trm4" bind x in t
-*)
+
(* example 5 from Terms.thy *)