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/Conformal_Mappings.thy
changeset 70365 4df0628e8545
parent 70347 e5cd5471c18a
child 70532 fcf3b891ccb1 
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -1000,7 +1000,7 @@
           done
         then show ?thesis
           apply (simp add: lim_at_infinity_0)
-          apply (rule Lim_eventually)
+          apply (rule tendsto_eventually)
           apply (simp add: eventually_at)
           apply (rule_tac x=r in exI)
           apply (simp add: \<open>0 < r\<close> dist_norm)
isabelle