--- a/src/HOL/Probability/Borel_Space.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Mar 18 22:11:46 2014 +0100
@@ -1111,7 +1111,7 @@
assumes "\<And>i. f i \<in> borel_measurable M"
shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
- unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
+ unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
lemma sets_Collect_eventually_sequentially[measurable]:
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"