--- a/src/HOL/Limits.thy Sat May 09 17:20:04 2020 +0000
+++ b/src/HOL/Limits.thy Mon May 11 11:15:41 2020 +0100
@@ -2240,7 +2240,7 @@
by (subst filterlim_cong[OF refl refl assms]) (rule refl)
lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f"
- by (auto simp: convergent_def LIMSEQ_Suc_iff)
+ by (auto simp: convergent_def filterlim_sequentially_Suc)
lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f"
proof (induct m arbitrary: f)