diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Probability/Sinc_Integral.thy --- a/src/HOL/Probability/Sinc_Integral.thy Tue Apr 25 08:38:23 2017 +0200 +++ b/src/HOL/Probability/Sinc_Integral.thy Tue Apr 25 16:39:54 2017 +0100 @@ -219,12 +219,11 @@ have *: "0 < x \ \x * sin t + cos t\ / (1 + x\<^sup>2) \ (x * 1 + 1) / 1" for x t :: real by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono) (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono) - then have **: "1 \ t \ 0 < x \ \?F x t\ \ exp (- x) * (x + 1)" for x t :: real + then have "1 \ t \ 0 < x \ \?F x t\ \ exp (- x) * (x + 1)" for x t :: real by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right intro!: mult_mono) - - show "\\<^sub>F i in at_top. AE x in lborel. 0 < x \ \?F x i\ \ exp (- x) * (x + 1)" - using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono) + then show "\\<^sub>F i in at_top. AE x in lborel. 0 < x \ \?F x i\ \ exp (- x) * (x + 1)" + by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"]) show "AE x in lborel. 0 < x \ (?F x \ 0) at_top" proof (intro always_eventually impI allI) fix x :: real assume "0 < x"