src/HOL/Nominal/Nominal.thy

--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 04 19:53:39 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 04 20:20:25 2006 +0100
@@ -195,6 +195,10 @@
   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"