diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Limits.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -2392,7 +2392,7 @@
     by (rule LIMSEQ_imp_Suc) (simp add: True)
 qed
 
-lemma LIMSEQ_power_zero: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_power_zero [tendsto_intros]: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
   for x :: "'a::real_normed_algebra_1"
   apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff)