--- a/src/HOL/OrderedGroup.thy Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Sat Mar 21 03:23:17 2009 -0700
@@ -316,6 +316,9 @@
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 *}
@@ -1296,7 +1299,7 @@
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)
@@ -1344,7 +1347,6 @@
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 {*