src/HOL/Probability/Independent_Family.thy

   shows indep_var_lebesgue_integral: "(\<integral>\<omega>. X1 \<omega> * X2 \<omega> \<partial>M) = (\<integral>\<omega>. X1 \<omega> \<partial>M) * (\<integral>\<omega>. X2 \<omega> \<partial>M)" (is ?eq)
     and indep_var_integrable: "integrable M (\<lambda>\<omega>. X1 \<omega> * X2 \<omega>)" (is ?int)
 unfolding indep_var_def
 proof -
   have *: "(\<lambda>\<omega>. X1 \<omega> * X2 \<omega>) = (\<lambda>\<omega>. \<Prod>i\<in>UNIV. (case_bool X1 X2 i \<omega>))"
-    by (simp add: UNIV_bool mult_commute)
+    by (simp add: UNIV_bool mult.commute)
   have **: "(\<lambda> _. borel) = case_bool borel borel"
     by (rule ext, metis (full_types) bool.simps(3) bool.simps(4))
   show ?eq
     apply (subst *)
     apply (subst indep_vars_lebesgue_integral)
     apply (auto)
     apply (subst **, subst indep_var_def [symmetric], rule assms)
     apply (simp split: bool.split add: assms)
-    by (simp add: UNIV_bool mult_commute)
+    by (simp add: UNIV_bool mult.commute)
   show ?int
     apply (subst *)
     apply (rule indep_vars_integrable)
     apply auto
     apply (subst **, subst indep_var_def [symmetric], rule assms)