diff -r 98dc38c250bb -r 35c570891a3a Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -523,6 +523,14 @@
   unfolding supp_Abs
   by auto
 
+lemma Abs_fresh_star_iff:
+  fixes x::"'a::fs"
+  shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"
+  unfolding fresh_star_def
+  by (auto simp add: Abs_fresh_iff)
+
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
   shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"