src/HOL/Rings.thy
changeset 62390 842917225d56
parent 62378 85ed00c1fe7c
child 62481 b5d8e57826df
     1.1 --- a/src/HOL/Rings.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -1578,7 +1578,7 @@
     1.4    by (simp add: not_less)
     1.5  
     1.6  proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
     1.7 -  by (auto simp add: abs_if split: split_if_asm)
     1.8 +  by (auto simp add: abs_if split: if_split_asm)
     1.9  
    1.10  lemma sum_squares_ge_zero:
    1.11    "0 \<le> x * x + y * y"