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/Transcendental.thy
changeset 72220 bb29e4eb938d
parent 72219 0f38c96a0a74
child 72980 4fc3dc37f406 
--- a/src/HOL/Transcendental.thy	Thu Aug 27 12:14:46 2020 +0100
+++ b/src/HOL/Transcendental.thy	Thu Aug 27 15:23:48 2020 +0100
@@ -1003,7 +1003,7 @@
   have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
     by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
   show ?thesis
-    using "*" by auto
+    using "*" by (auto cong: Lim_cong_within)
 qed
isabelle