--- a/src/HOL/Probability/Stream_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Stream_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -279,7 +279,7 @@
simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
lemma sets_stream_space_eq: "sets (stream_space M) =
- sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+ sets (SUP i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
simp: space_Sup_eq_UN space_stream_space)