diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -57,36 +57,6 @@
 is
   "permute_bn3_raw"
 
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]