src/HOL/Nominal/Nominal.thy

   done
 
 lemma fresh_set_empty:
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)
+
+lemma fresh_singleton:
+  shows "a\<sharp>{x} = a\<sharp>x"
+  by (simp add: fresh_def supp_singleton)
 
 lemma fresh_prod:
   fixes a :: "'x"
   and   x :: "'a"
   and   y :: "'b"