--- a/Nominal/Ex/Foo1.thy	Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Tue Dec 07 14:27:39 2010 +0000
@@ -35,6 +35,7 @@
 | "bn4 (BNil) = {}"
 | "bn4 (BAs a as) = {atom a} \<union> bn4 as"
 
+thm foo.permute_bn
 thm foo.perm_bn_alpha
 thm foo.perm_bn_simps
 thm foo.bn_finite
@@ -55,43 +56,6 @@
 thm foo.fresh
 thm foo.bn_finite
 
-
-lemma tt1:
-  shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt2:
-  shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt3:
-  shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt4:
-  shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)"
-apply(induct as rule: foo.inducts(3))
-apply(auto)[8]
-apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq)
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt insert_eqvt)
-done
-
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P"