src/HOL/Probability/Finite_Product_Measure.thy
changeset 61565 352c73a689da
parent 61424 c3658c18b7bc
child 61808 fc1556774cfe
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
     1.3 @@ -829,7 +829,7 @@
     1.4    fixes M :: "'i \<Rightarrow> 'a measure"
     1.5    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
     1.6  
     1.7 -sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
     1.8 +sublocale product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
     1.9    by (rule sigma_finite_measures)
    1.10  
    1.11  locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +