src/HOL/OrderedGroup.thy

 
 lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b"
 by (simp add: diff_minus add_ac)
 
 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
+by (simp add: algebra_simps)
+
+lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
 by (simp add: algebra_simps)
 
 end
 
 subsection {* (Partially) Ordered Groups *} 

 apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
 apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
 done
 
 lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
+by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
 
 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
 by (simp add: diff_minus)
 
 lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"

 by (auto intro: add_strict_right_mono add_strict_left_mono
   add_less_le_mono add_le_less_mono add_strict_mono)
 
 text{*Simplification of @{term "x-y < 0"}, etc.*}
 lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
 lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
 
 ML {*
 structure ab_group_add_cancel = Abel_Cancel
 (