--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jul 17 14:02:42 2019 +0100
@@ -7447,7 +7447,7 @@
by (simp add: filterlim_at_top)
with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
by (auto elim!: eventually_mono simp: f_def)
- thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
+ thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: tendsto_eventually)
next
have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
proof (cases "n \<ge> a")