--- a/src/HOL/Transcendental.thy Tue May 11 19:01:35 2010 -0700
+++ b/src/HOL/Transcendental.thy Tue May 11 19:38:16 2010 -0700
@@ -732,7 +732,8 @@
also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq)
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto
also have "\<dots> < r /3 + r/3 + r/3"
- using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` by auto
+ using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
+ by (rule add_strict_mono [OF add_less_le_mono])
finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r"
by auto
} thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>