src/HOL/Rings.thy
changeset 51520 e9b361845809
parent 50420 f1a27e82af16
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Rings.thy	Tue Mar 26 12:20:53 2013 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Mar 26 12:20:54 2013 +0100
     1.3 @@ -1143,6 +1143,10 @@
     1.4    "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
     1.5    by (simp add: abs_mult)
     1.6  
     1.7 +lemma abs_diff_less_iff:
     1.8 +  "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
     1.9 +  by (auto simp add: diff_less_eq ac_simps abs_less_iff)
    1.10 +
    1.11  end
    1.12  
    1.13  code_modulename SML