src/HOL/Analysis/Complex_Transcendental.thy
changeset 66611 c375b64a6c24
parent 66480 4b8d1df8933b
child 66793 deabce3ccf1f
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 15:12:40 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 16:41:40 2017 +0200
     1.3 @@ -752,7 +752,7 @@
     1.4  lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
     1.5    using Taylor_exp [of 1 14] exp_le
     1.6    apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
     1.7 -  apply (simp only: pos_le_divide_eq [symmetric], linarith)
     1.8 +  apply (simp only: pos_le_divide_eq [symmetric])
     1.9    done
    1.10  
    1.11  lemma e_less_272: "exp 1 < (272/100::real)"