--- a/Nominal/Nominal2_Eqvt.thy	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Jan 03 16:19:27 2011 +0000
@@ -24,9 +24,9 @@
 section {* eqvt lemmas *}
 
 lemmas [eqvt] =
-  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
+  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt
   imp_eqvt[folded induct_implies_def]
-  uminus_eqvt
+  all_eqvt[folded induct_forall_def]
 
   (* nominal *)
   supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
@@ -41,6 +41,7 @@
   (* fsets *)
   permute_fset fset_eqvt
 
+
 text {* helper lemmas for the perm_simp *}
 
 definition