# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1563377526 -3600
# Node ID 81b65ddac59fae8ceaa40402745e6daa7f307ea0
# Parent  89830f937e6824fe0e6c9c97f47b6fdc41868ee1
fixed renaming issues

diff -r 89830f937e68 -r 81b65ddac59f src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jul 17 16:32:06 2019 +0100
@@ -2631,7 +2631,7 @@
   have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
   proof (rule Lim_transform_bound)
     show "(inverse o real) \<longlonglongrightarrow> 0"
-      by (metis comp_def lim_inverse_n tendsto_explicit)
+      by (metis comp_def lim_inverse_n lim_explicit)
     show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
     proof
       fix n::nat
diff -r 89830f937e68 -r 81b65ddac59f src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 17 16:32:06 2019 +0100
@@ -3172,7 +3172,7 @@
     and "f0 \<in> S"
   obtains N where "\<forall>n\<ge>N. f n \<in> S"
   using assms using tendsto_def
-  using tendsto_explicit[of f f0] assms by auto
+  using lim_explicit[of f f0] assms by auto
 
 lemma ereal_LimI_finite_iff:
   fixes x :: ereal
diff -r 89830f937e68 -r 81b65ddac59f src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Jul 17 16:32:06 2019 +0100
@@ -1145,7 +1145,7 @@
 lemma lim_def: "lim X = (THE L. X \<longlonglongrightarrow> L)"
   unfolding Lim_def ..
 
-lemma tendsto_explicit:
+lemma lim_explicit:
   "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
   unfolding tendsto_def eventually_sequentially by auto