--- a/Nominal/Test.thy	Mon Mar 08 11:12:15 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 08 11:25:57 2010 +0100
@@ -499,8 +499,8 @@
   "bp (PVar x) = {atom x}"
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
+thm alpha_exp_raw_alpha_pat_raw.intros
 
-thm quot_respect
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
   EVar name
@@ -516,6 +516,7 @@
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+thm alpha_exp6_raw_alpha_pat6_raw.intros
 
 (* example 7 from Peter Sewell's bestiary *)
 nominal_datatype exp7 =
@@ -535,6 +536,7 @@
   "b7 (Assign x e) = {atom x}"
 | "b7s (Single a) = b7 a"
 | "b7s (More a as) = (b7 a) \<union> (b7s as)"
+thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
 
 (* example 8 from Peter Sewell's bestiary *)
 nominal_datatype exp8 =
@@ -572,6 +574,7 @@
 | "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}"
+thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros