--- a/Nominal/Abs.thy	Fri Mar 19 12:31:17 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 19 12:31:55 2010 +0100
@@ -1,5 +1,5 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" "Nominal2_FSet"
 begin
 
 lemma permute_boolI:
@@ -749,17 +749,6 @@
 
 (* support of concrete atom sets *)
 
-lemma atom_eqvt_raw:
-  fixes p::"perm"
-  shows "(p \<bullet> atom) = atom"
-by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-apply(rule inj_image_eq_iff)
-apply(simp add: inj_on_def)
-done
-
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
@@ -793,5 +782,10 @@
   \<and> pi \<bullet> bs = cs)"
 by (simp add: alpha_gen)
 
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 end