--- a/src/HOL/Probability/Probability_Measure.thy Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Nov 04 08:13:49 2015 +0100
@@ -461,7 +461,7 @@
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
-sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2"
proof
show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"
by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
@@ -471,7 +471,7 @@
fixes I :: "'i set"
assumes prob_space: "\<And>i. prob_space (M i)"
-sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
+sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i
by (rule prob_space)
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I