--- a/src/HOL/Probability/Distributions.thy Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Probability/Distributions.thy Wed Jul 17 14:02:42 2019 +0100
@@ -116,7 +116,7 @@
show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
apply (intro nn_integral_LIMSEQ)
apply (auto simp: incseq_def le_fun_def eventually_sequentially
- split: split_indicator intro!: Lim_eventually)
+ split: split_indicator intro!: tendsto_eventually)
apply (metis nat_ceiling_le_eq)
done