--- a/src/HOL/OrderedGroup.thy Thu Sep 04 16:43:51 2008 +0200
+++ b/src/HOL/OrderedGroup.thy Thu Sep 04 17:18:44 2008 +0200
@@ -234,6 +234,12 @@
thus ?thesis by (simp add: eq_commute)
qed
+lemma diff_add_cancel: "a - b + b = a"
+ by (simp add: diff_minus add_assoc)
+
+lemma add_diff_cancel: "a + b - b = a"
+ by (simp add: diff_minus add_assoc)
+
end
class ab_group_add = minus + uminus + comm_monoid_add +
@@ -283,12 +289,6 @@
lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
by (simp add: diff_minus add_ac)
-lemma diff_add_cancel: "a - b + b = a"
- by (simp add: diff_minus add_ac)
-
-lemma add_diff_cancel: "a + b - b = a"
- by (simp add: diff_minus add_ac)
-
lemmas compare_rls =
diff_minus [symmetric]
add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2