--- a/Quot/Nominal/Nominal2_Base.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Nominal2_Base.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -859,17 +859,32 @@
   shows "supp (0::perm) = {}"
   unfolding supp_perm by simp
 
+lemma fresh_plus_perm:
+  fixes p q::perm
+  assumes "a \<sharp> p" "a \<sharp> q"
+  shows "a \<sharp> (p + q)"
+  using assms
+  unfolding fresh_def
+  by (auto simp add: supp_perm)
+
 lemma supp_plus_perm:
   fixes p q::perm
   shows "supp (p + q) \<subseteq> supp p \<union> supp q"
   by (auto simp add: supp_perm)
 
+lemma fresh_minus_perm:
+  fixes p::perm
+  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
+  unfolding fresh_def
+  apply(auto simp add: supp_perm)
+  apply(metis permute_minus_cancel)+
+  done
+
 lemma supp_minus_perm:
   fixes p::perm
   shows "supp (- p) = supp p"
-  apply(auto simp add: supp_perm)
-  apply(metis permute_minus_cancel)+
-  done
+  unfolding supp_conv_fresh
+  by (simp add: fresh_minus_perm)
 
 instance perm :: fs
 by default (simp add: supp_perm finite_perm_lemma)