src/HOL/Rings.thy
changeset 61762 d50b993b4fb9
parent 61649 268d88ec9087
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Rings.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -1559,6 +1559,9 @@
     1.4  lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
     1.5    by (simp add: not_less)
     1.6  
     1.7 +proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
     1.8 +  by (auto simp add: abs_if split: split_if_asm)
     1.9 +
    1.10  end
    1.11  
    1.12  class linordered_ring_strict = ring + linordered_semiring_strict