--- a/Nominal/Ex/ExNotRsp.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-theory ExNotRsp
-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
-
-
-