# HG changeset patch
# User huffman
# Date 1237630997 25200
# Node ID 5cd9b19edef3b582601de4556cd32fe26830108b
# Parent  40a1865ab1221eba6190356fb47b4f3ada9606d5
move diff_eq_0_iff_eq into class locale context

diff -r 40a1865ab122 -r 5cd9b19edef3 src/HOL/OrderedGroup.thy
--- 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 {*