--- a/src/HOL/Probability/Distribution_Functions.thy Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy Thu Jun 28 17:14:40 2018 +0100
@@ -107,7 +107,7 @@
using \<open>decseq f\<close> unfolding cdf_def
by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(\<Inter>i. {.. f i}) = {.. a}"
- using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+ using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
by (simp add: cdf_def)
qed simp