--- a/Nominal/Nominal2_Base.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -1411,6 +1411,16 @@
 unfolding fresh_star_def
 by (simp add: fresh_set)
 
+lemma fresh_star_singleton:
+  fixes a::"atom"
+  shows "as \<sharp>* {a} \<longleftrightarrow> as \<sharp>* a"
+  by (simp add: fresh_star_def fresh_finite_insert fresh_set_empty)
+
+lemma fresh_star_fset:
+  fixes xs::"('a::fs) list"
+  shows "as \<sharp>* fset S \<longleftrightarrow> as \<sharp>* S"
+by (simp add: fresh_star_def fresh_def) 
+
 lemma fresh_star_Un:
   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
   by (auto simp add: fresh_star_def)
@@ -1701,7 +1711,6 @@
 
 section {* Renaming permutations *}
 
-
 lemma set_renaming_perm:
   assumes a: "p \<bullet> bs \<inter> bs = {}" 
   and     b: "finite bs"
@@ -1840,6 +1849,10 @@
   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
   by (simp add: fresh_def supp_at_base supp_atom)
 
+lemma fresh_star_atom_at_base: 
+  fixes b::"'a::at_base"
+  shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b"
+  by (simp add: fresh_star_def fresh_atom_at_base)
 
 instance at_base < fs
 proof qed (simp add: supp_at_base)