--- 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