src/HOL/Hyperreal/MacLaurin.thy
changeset 15081 32402f5624d1
parent 15079 2ef899e4526d
child 15131 c69542757a4d
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:28 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:40 2004 +0200
@@ -575,12 +575,12 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma sin_bound_lemma:
-    "[|x = y; abs u \<le> (v::real) |] ==> abs ((x + u) - y) \<le> v"
+    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
 by auto
 
 lemma Maclaurin_sin_bound:
   "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-  x ^ m))  \<le> inverse(real (fact n)) * abs(x) ^ n"
+  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
 proof -
   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
     by (rule_tac mult_right_mono,simp_all)