diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/Nominal2_Base.thy	Sun Dec 15 15:14:40 2013 +1100
@@ -272,7 +272,7 @@
 
 lemma permute_diff [simp]:
   shows "(p - q) \<bullet> x = p \<bullet> - q \<bullet> x"
-  unfolding diff_minus by simp
+  using permute_plus [of p "- q" x] by simp
 
 lemma permute_minus_cancel [simp]:
   shows "p \<bullet> - p \<bullet> x = x"
@@ -365,7 +365,7 @@
 instance
 apply default
 apply (simp add: permute_perm_def)
-apply (simp add: permute_perm_def diff_minus minus_add add_assoc)
+apply (simp add: permute_perm_def algebra_simps)
 done
 
 end
@@ -373,12 +373,12 @@
 lemma permute_self: 
   shows "p \<bullet> p = p"
   unfolding permute_perm_def 
-  by (simp add: diff_minus add_assoc)
+  by (simp add: add_assoc)
 
 lemma pemute_minus_self:
   shows "- p \<bullet> p = p"
   unfolding permute_perm_def 
-  by (simp add: diff_minus add_assoc)
+  by (simp add: add_assoc)
 
 
 subsection {* Permutations for functions *}
@@ -870,7 +870,8 @@
   fixes p q::"perm"
   shows "p \<bullet> (- q) = - (p \<bullet> q)"
   unfolding permute_perm_def
-  by (simp add: diff_minus minus_add add_assoc)
+  by (simp add: diff_add_eq_diff_diff_swap)
+
 
 subsubsection {* Equivariance of Logical Operators *}