--- a/Nominal/Test.thy	Thu Mar 04 15:31:34 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 15:56:58 2010 +0100
@@ -4,7 +4,7 @@
 
 text {* weirdo example from Peter Sewell's bestiary *}
 
-(*nominal_datatype weird =
+nominal_datatype weird =
   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
     bind x in p1, bind x in p2, bind y in p2, bind y in p3
 | WV "name"
@@ -19,7 +19,7 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}
 thm weird_inj
 
-local_setup {*
+(*local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),
 build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}
 
@@ -144,10 +144,11 @@
 thm permute_lam_raw_permute_bp_raw.simps
 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
-thm lam_bp_induct
+(*thm lam_bp_induct
 thm lam_bp_perm
 thm lam_bp_fv
 thm lam_bp_bn
+thm lam_bp_inject*)
 
 text {* example 2 *}
 
@@ -171,10 +172,11 @@
 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
-thm trm'_pat'_induct
+(*thm trm'_pat'_induct
 thm trm'_pat'_perm
 thm trm'_pat'_fv
 thm trm'_pat'_bn
+thm trm'_pat'_inject*)
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -193,10 +195,10 @@
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
 thm f0_raw.simps
-thm trm0_pat0_induct
+(*thm trm0_pat0_induct
 thm trm0_pat0_perm
 thm trm0_pat0_fv
-thm trm0_pat0_bn
+thm trm0_pat0_bn*)
 
 text {* example type schemes *}
 
@@ -210,12 +212,11 @@
 *)
 
 
-(* alpha_eqvt fails...
 nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 and  tyS = 
-  All xs::"name set" ty::"t" bind xs in ty *)
+  All xs::"name set" ty::"t" bind xs in ty
 
 (* example 1 from Terms.thy *)
 
@@ -271,13 +272,13 @@
 
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)
-(*nominal_datatype trm4 =
+nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
 
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 
 (* example 5 from Terms.thy *)
 
@@ -296,7 +297,7 @@
 
 (* example 6 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype trm6 =
   Vr6 "name"
 | Lm6 x::"name" t::"trm6"         bind x in t
@@ -306,11 +307,10 @@
 where
   "bv6 (Vr6 n) = {}"
 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" *)
-
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
 (* example 7 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype trm7 =
   Vr7 "name"
 | Lm7 l::"name" r::"trm7"   bind l in r
@@ -320,7 +320,7 @@
 where
   "bv7 (Vr7 n) = {atom n}"
 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" *)
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
 
 (* example 8 from Terms.thy *)
 
@@ -338,7 +338,7 @@
 
 (* example 9 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype lam9 =
   Var9 "name"
 | Lam9 n::"name" l::"lam9" bind n in l
@@ -348,13 +348,13 @@
   bv9
 where
   "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}" *)
+| "bv9 (Lam9 x b) = {atom x}"
 
 (* example from my PHD *)
 
 atom_decl coname
 
-(*nominal_datatype phd =
+nominal_datatype phd =
    Ax "name" "coname"
 |  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
 |  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
@@ -365,7 +365,7 @@
 
 thm alpha_phd_raw.intros[no_vars]
 thm fv_phd_raw.simps[no_vars]
-*)
+
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -501,7 +501,7 @@
 
 thm quot_respect
 (* example 6 from Peter Sewell's bestiary *)
-(*nominal_datatype exp6 =
+nominal_datatype exp6 =
   EVar name
 | EPair exp6 exp6
 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
@@ -514,10 +514,10 @@
 where
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"*)
+| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
 (* example 7 from Peter Sewell's bestiary *)
-(*nominal_datatype exp7 =
+nominal_datatype exp7 =
   EVar name
 | EUnit
 | EPair exp7 exp7
@@ -533,10 +533,10 @@
 where
   "b7 (Assign x e) = {atom x}"
 | "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"*)
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
 
 (* example 8 from Peter Sewell's bestiary *)
-(*nominal_datatype exp8 =
+nominal_datatype exp8 =
   EVar name
 | EUnit
 | EPair exp8 exp8
@@ -570,7 +570,7 @@
 | "b_fnclauses (S fc) = (b_fnclause fc)"
 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"*)
+| "b_fnclause (K x pat exp8) = {atom x}"