--- a/Nominal/Ex/Foo2.thy	Sun Nov 28 16:37:34 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 29 05:10:02 2010 +0000
@@ -26,7 +26,6 @@
 
 thm foo.perm_bn_simps
 
-
 thm foo.distinct
 thm foo.induct
 thm foo.inducts
@@ -246,7 +245,9 @@
 apply(rule conjI)
 apply(assumption)
 apply(simp add: foo.eq_iff)
-defer
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(4))
@@ -285,7 +286,9 @@
 apply(rule conjI)
 apply(assumption)
 apply(rule uu1)
-defer
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(5))
@@ -317,7 +320,10 @@
 apply(assumption)
 apply(simp add: fresh_star_prod)
 apply(simp add: fresh_star_def)
-sorry
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
+done