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