# HG changeset patch
# User huffman
# Date 1273631896 25200
# Node ID 99745a4b9cc98e818a800186794a53096656c198
# Parent  02df88789641b73fc40a612c3fa9c7cb7cf37118
fix some linarith_split_limit warnings

diff -r 02df88789641 -r 99745a4b9cc9 src/HOL/Transcendental.thy
--- 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>