# HG changeset patch
# User haftmann
# Date 1573295931 0
# Node ID b7d481cdd54d11d2d81dc623a9ecda7dcd5fcdee
# Parent  3c04a52c422ad9f9743bcf26a398c57611dda445
new lemma

diff -r 3c04a52c422a -r b7d481cdd54d src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Nov 08 20:59:34 2019 +0100
+++ b/src/HOL/Groups.thy	Sat Nov 09 10:38:51 2019 +0000
@@ -606,6 +606,10 @@
   "(a - b) + c = (a + c) - b"
   by (simp add: algebra_simps)
 
+lemma minus_diff_commute:
+  "- b - a = - a - b"
+  by (simp only: diff_conv_add_uminus add.commute)
+
 end
 
 
diff -r 3c04a52c422a -r b7d481cdd54d src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Fri Nov 08 20:59:34 2019 +0100
+++ b/src/HOL/ex/Word.thy	Sat Nov 09 10:38:51 2019 +0000
@@ -11,15 +11,6 @@
 
 subsection \<open>Preliminaries\<close>
 
-context ab_group_add
-begin
-
-lemma minus_diff_commute:
-  "- b - a = - a - b"
-  by (simp only: diff_conv_add_uminus add.commute)
-
-end
-
 lemma take_bit_uminus:
   "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)