diff -r 8f647d24b49f -r 32b4185bfdc7 src/HOL/OrderedGroup.thy
--- 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