--- a/src/HOL/Probability/Distributions.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Distributions.thy Tue Dec 29 23:04:53 2015 +0100
@@ -116,7 +116,7 @@
shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)"
proof (rule LIMSEQ_unique)
let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
- show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
+ show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ereal (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)
@@ -126,7 +126,7 @@
have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
(1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
by (intro tendsto_intros tendsto_power_div_exp_0) simp
- then show "?X ----> real_of_nat (fact k)"
+ then show "?X \<longlonglongrightarrow> real_of_nat (fact k)"
by (subst nn_intergal_power_times_exp_Icc)
(auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
qed