Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted to better linear arith
authornipkow
Thu, 07 Sep 2017 16:41:40 +0200
changeset 66611 c375b64a6c24
parent 66610 98b7ba7b1e9a
child 66612 84926115c2dd
adapted to better linear arith
src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 15:12:40 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 07 16:41:40 2017 +0200
@@ -752,7 +752,7 @@
 lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
   using Taylor_exp [of 1 14] exp_le
   apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
-  apply (simp only: pos_le_divide_eq [symmetric], linarith)
+  apply (simp only: pos_le_divide_eq [symmetric])
   done
 
 lemma e_less_272: "exp 1 < (272/100::real)"
isabelle