--- a/src/HOL/OrderedGroup.thy Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/OrderedGroup.thy Fri Dec 18 19:00:11 2009 -0800
@@ -193,7 +193,7 @@
assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
qed
-lemma equals_zero_I:
+lemma minus_unique:
assumes "a + b = 0" shows "- a = b"
proof -
have "- a = - a + (a + b)" using assms by simp
@@ -201,6 +201,8 @@
finally show ?thesis .
qed
+lemmas equals_zero_I = minus_unique (* legacy name *)
+
lemma diff_self [simp]: "a - a = 0"
by (simp add: diff_minus)
@@ -291,7 +293,7 @@
lemma minus_add_distrib [simp]:
"- (a + b) = - a + - b"
-by (rule equals_zero_I) (simp add: add_ac)
+by (rule minus_unique) (simp add: add_ac)
lemma minus_diff_eq [simp]:
"- (a - b) = b - a"