src/HOL/Transcendental.thy
changeset 36842 99745a4b9cc9
parent 36824 2e9a866141b8
child 36970 fb3fdb4b585e
     1.1 --- a/src/HOL/Transcendental.thy	Tue May 11 19:01:35 2010 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Tue May 11 19:38:16 2010 -0700
     1.3 @@ -732,7 +732,8 @@
     1.4      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)
     1.5      also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto
     1.6      also have "\<dots> < r /3 + r/3 + r/3" 
     1.7 -      using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` by auto
     1.8 +      using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
     1.9 +      by (rule add_strict_mono [OF add_less_le_mono])
    1.10      finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r"
    1.11        by auto
    1.12    } thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>