Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 65583 8d53b3bebab4
parent 65578 e4997c181cce
child 65585 a043de9ad41e 
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -407,7 +407,7 @@
     then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
       by (metis exp_less_mono exp_ln that)
     then show ?thesis
-      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
+      by (simp add: \<delta>01(1) \<open>0 < k\<close> exp_of_nat_mult)
   qed
   { fix t and e::real
     assume "e>0"
isabelle