--- a/src/HOL/Groups.thy Sat Aug 20 12:51:15 2011 -0700
+++ b/src/HOL/Groups.thy Sat Aug 20 13:07:00 2011 -0700
@@ -411,6 +411,10 @@
ultimately show "a = - b" by simp
qed
+lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
+ unfolding eq_neg_iff_add_eq_0 [symmetric]
+ by (rule equation_minus_iff)
+
end
class ab_group_add = minus + uminus + comm_monoid_add +
@@ -466,7 +470,7 @@
(* FIXME: duplicates right_minus_eq from class group_add *)
(* but only this one is declared as a simp rule. *)
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
-by (simp add: algebra_simps)
+ by (rule right_minus_eq)
lemma diff_eq_diff_eq:
"a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
--- a/src/HOL/RealDef.thy Sat Aug 20 12:51:15 2011 -0700
+++ b/src/HOL/RealDef.thy Sat Aug 20 13:07:00 2011 -0700
@@ -1612,12 +1612,6 @@
shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
by (simp add: algebra_simps)
-text {* TODO: move elsewhere *}
-lemma add_eq_0_iff:
- fixes x y :: "'a::group_add"
- shows "x + y = 0 \<longleftrightarrow> y = - x"
-by (auto dest: minus_unique)
-
text {* FIXME: declare this [simp] for all types, or not at all *}
lemma real_two_squares_add_zero_iff [simp]:
"(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"