src/HOL/Analysis/Harmonic_Numbers.thy
changeset 65109 a79c1080f1e9
parent 64267 b9a1486e79be
child 65273 917ae0ba03a2
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Mar 02 21:16:02 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Sun Mar 05 10:57:51 2017 +0100
     1.3 @@ -533,7 +533,7 @@
     1.4  lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
     1.5    and euler_mascheroni_less_13_over_22: "(euler_mascheroni :: real) < 13/22" (is ?th2)
     1.6  proof -
     1.7 -  have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric] powr_numeral)
     1.8 +  have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric])
     1.9    also from ln_approx_bounds[of 2 3] have "\<dots> \<in> {3*307/443<..<3*4615/6658}"
    1.10      by (simp add: eval_nat_numeral)
    1.11    finally have "ln (real (Suc 7)) \<in> \<dots>" .