src/HOL/Probability/Finite_Product_Measure.thy

   by (simp add: subset_eq Pi_iff)
 
 lemma sets_in_Pi[measurable (raw)]:
   "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
-  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
+  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
 
 lemma sets_in_extensional_aux:
   "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"

     by (auto simp add: extensional_def space_PiM)
   then show ?thesis by simp
 qed
 
 lemma sets_in_extensional[measurable (raw)]:
-  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
+  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
 
 locale product_sigma_finite =
   fixes M :: "'i \<Rightarrow> 'a measure"