src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Rings.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1559,7 +1559,7 @@
 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"
+proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: split_if_asm)
 
 end