diff -r 082d9fd28f89 -r ebf253d80670 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Jul 30 00:40:32 2010 +0100
@@ -58,12 +58,18 @@
   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
   by (rule, simp_all add: fresh_star_prod)
 
+lemma fresh_star_zero:
+  shows "as \<sharp>* (0::perm)"
+  unfolding fresh_star_def
+  by (simp add: fresh_zero_perm)
+
 lemma fresh_star_plus:
   fixes p q::perm
   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
   unfolding fresh_star_def
   by (simp add: fresh_plus_perm)
 
+
 lemma fresh_star_permute_iff:
   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
   unfolding fresh_star_def