1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:28 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:40 2004 +0200
     1.3 @@ -575,12 +575,12 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  lemma sin_bound_lemma:
     1.7 -    "[|x = y; abs u \<le> (v::real) |] ==> abs ((x + u) - y) \<le> v"
     1.8 +    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
     1.9  by auto
    1.10  
    1.11  lemma Maclaurin_sin_bound:
    1.12    "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.13 -  x ^ m))  \<le> inverse(real (fact n)) * abs(x) ^ n"
    1.14 +  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
    1.15  proof -
    1.16    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
    1.17      by (rule_tac mult_right_mono,simp_all)