diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/NoneExamples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/NoneExamples.thy	Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,54 @@
+theory NoneExamples
+imports "../NewParser"
+begin
+
+atom_decl name
+
+(* this example binds bound names and
+   so is not respectful *)
+(*
+nominal_datatype trm =
+  Vr "name"
+| Lm x::"name" t::"trm"         bind x in t
+| Lt left::"trm" right::"trm"   bind "bv left" in right
+binder
+  bv
+where
+  "bv (Vr n) = {}"
+| "bv (Lm n t) = {atom n} \<union> bv t"
+| "bv (Lt l r) = bv l \<union> bv r"
+*)
+
+(* this example uses "-" in the binding function; 
+   at the moment this is unsupported *)
+(*
+nominal_datatype trm' =
+  Vr' "name"
+| Lm' l::"name" r::"trm'"   bind l in r
+| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
+binder
+  bv'
+where
+  "bv' (Vr' n) = {atom n}"
+| "bv' (Lm' n t) = bv' t - {atom n}"
+| "bv' (Lt' l r) = bv' l \<union> bv' r"
+*)
+
+(* this example again binds bound names  *)
+(*
+nominal_datatype trm'' =
+  Va'' "name"
+| Lm'' n::"name" l::"trm''" bind n in l
+and bla'' =
+  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+binder
+  bv''
+where
+  "bv'' (Vm'' x) = {}"
+| "bv'' (Lm'' x b) = {atom x}"
+*)
+
+end
+
+
+