diff -r 8b5a1ad60487 -r e33e37fd4c7d Nominal/ExNotRsp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExNotRsp.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,48 @@
+theory ExNotRsp
+imports "Parser"
+begin
+
+atom_decl name
+
+(* example 6 from Terms.thy *)
+
+nominal_datatype trm6 =
+  Vr6 "name"
+| Lm6 x::"name" t::"trm6"         bind x in t
+| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+binder
+  bv6
+where
+  "bv6 (Vr6 n) = {}"
+| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
+
+(* example 7 from Terms.thy *)
+nominal_datatype trm7 =
+  Vr7 "name"
+| Lm7 l::"name" r::"trm7"   bind l in r
+| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
+binder
+  bv7
+where
+  "bv7 (Vr7 n) = {atom n}"
+| "bv7 (Lm7 n t) = bv7 t - {atom n}"
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+*)
+
+(* example 9 from Terms.thy *)
+nominal_datatype lam9 =
+  Var9 "name"
+| Lam9 n::"name" l::"lam9" bind n in l
+and bla9 =
+  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+binder
+  bv9
+where
+  "bv9 (Var9 x) = {}"
+| "bv9 (Lam9 x b) = {atom x}"
+
+end
+
+
+