--- a/Nominal/Nominal2_Base.thy	Thu Jan 06 11:00:16 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Jan 06 13:28:04 2011 +0000
@@ -1389,6 +1389,11 @@
   unfolding supp_def
   by simp
 
+lemma fresh_empty_fset:
+  shows "a \<sharp> {||}"
+unfolding fresh_def
+by (simp)
+
 lemma supp_insert_fset [simp]:
   fixes x::"'a::fs"
   and   S::"'a fset"
@@ -1397,6 +1402,13 @@
   apply(simp add: supp_of_finite_insert)
   done
 
+lemma fresh_insert_fset:
+  fixes x::"'a::fs"
+  and   S::"'a fset"
+  shows "a \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+  unfolding fresh_def
+  by (simp)
+
 lemma fset_finite_supp:
   fixes S::"('a::fs) fset"
   shows "finite (supp S)"