--- a/Nominal-General/Nominal2_Base.thy	Thu Jun 03 11:48:44 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Thu Jun 03 15:02:52 2010 +0200
@@ -385,6 +385,11 @@
   unfolding permute_perm_def
   by (auto simp add: swap_atom expand_perm_eq)
 
+lemma uminus_eqvt:
+  fixes p q::"perm"
+  shows "p \<bullet> (- q) = - (p \<bullet> q)"
+  unfolding permute_perm_def
+  by (simp add: diff_minus minus_add add_assoc)
 
 subsection {* Permutations for functions *}
 

--- a/Nominal-General/Nominal2_Eqvt.thy	Thu Jun 03 11:48:44 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu Jun 03 15:02:52 2010 +0200
@@ -295,14 +295,13 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_unit)
 
-
 section {* additional eqvt lemmas *}
 
 lemmas [eqvt] = 
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt
+  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
 
   (* datatypes *)
   Pair_eqvt permute_list.simps