--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Dec 29 23:04:53 2015 +0100
@@ -187,7 +187,7 @@
lemma measure_PiM_countable:
fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets M"
- shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) ----> measure S (Pi UNIV E)"
+ shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) \<longlonglongrightarrow> measure S (Pi UNIV E)"
proof -
let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^sub>E {.. n} E)"
have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"