src/HOL/Analysis/Gamma_Function.thy
 changeset 65578 e4997c181cce parent 64969 a6953714799d child 65587 16a8991ab398
```     1.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1880,7 +1880,7 @@
1.4    show "G x \<ge> Gamma x"
1.5    proof (rule tendsto_upperbound)
1.6      from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
1.7 -      using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
1.8 +      using  x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "1::nat"]])
1.10  next
1.11    show "G x \<le> Gamma x"
1.12 @@ -1891,7 +1891,7 @@
1.13      thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
1.14    next
1.15      from G_upper[of x] show "eventually (\<lambda>n. Gamma_series x n * (1 + x / real n) \<ge> G x) sequentially"
1.16 -      using eventually_ge_at_top[of "2::nat"] x by (auto elim!: eventually_mono)
1.17 +      using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "2::nat"]])
1.18    qed simp_all
1.19  qed
1.20
1.21 @@ -2472,9 +2472,9 @@
1.22    let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
1.23    from z have z': "z \<noteq> 0" by auto
1.24
1.25 -  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"]
1.26 +  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
1.27      using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
1.28 -                     elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int)
1.29 +                     intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
1.30    moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
1.31      by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
1.32    ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
```