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