src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Rings.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -1559,6 +1559,9 @@
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
 
+proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
+  by (auto simp add: abs_if split: split_if_asm)
+
 end
 
 class linordered_ring_strict = ring + linordered_semiring_strict