# HG changeset patch
# User huffman
# Date 1261191611 28800
# Node ID 14595e0c27e877832883fcb006e2ef6895ac6522
# Parent  402b7c74799db70a3a2e17a38d8c8e329c24d053
rename equals_zero_I to minus_unique (keep old name too)

diff -r 402b7c74799d -r 14595e0c27e8 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/Library/FrechetDeriv.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -438,7 +438,7 @@
     hence 2: "x + h \<noteq> 0"
       apply (rule contrapos_nn)
       apply (rule sym)
-      apply (erule equals_zero_I)
+      apply (erule minus_unique)
       done
     show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
           = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
diff -r 402b7c74799d -r 14595e0c27e8 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/NSA/NSA.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -1711,7 +1711,7 @@
 lemma Infinitesimal_add_not_zero:
      "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> star_of x + h \<noteq> 0"
 apply auto
-apply (subgoal_tac "h = - star_of x", auto intro: equals_zero_I [symmetric])
+apply (subgoal_tac "h = - star_of x", auto intro: minus_unique [symmetric])
 done
 
 lemma Infinitesimal_square_cancel [simp]:
diff -r 402b7c74799d -r 14595e0c27e8 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/NSA/NSComplex.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -161,7 +161,7 @@
 
 lemma hcomplex_add_minus_eq_minus:
       "x + y = (0::hcomplex) ==> x = -y"
-apply (drule OrderedGroup.equals_zero_I)
+apply (drule OrderedGroup.minus_unique)
 apply (simp add: minus_equation_iff [of x y])
 done
 
diff -r 402b7c74799d -r 14595e0c27e8 src/HOL/OrderedGroup.thy
--- 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"
diff -r 402b7c74799d -r 14595e0c27e8 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -228,10 +228,10 @@
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
+by (rule minus_unique) (simp add: left_distrib [symmetric]) 
 
 lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
+by (rule minus_unique) (simp add: right_distrib [symmetric]) 
 
 text{*Extract signs from products*}
 lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]