src/HOL/Probability/Bochner_Integration.thy

 lemma (in pair_sigma_finite) integrable_product_swap:
   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
   assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
+  interpret Q: pair_sigma_finite M2 M1 ..
   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
   show ?thesis unfolding *
     by (rule integrable_distr[OF measurable_pair_swap'])
        (simp add: distr_pair_swap[symmetric] assms)
 qed
 
 lemma (in pair_sigma_finite) integrable_product_swap_iff:
   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
   shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
+  interpret Q: pair_sigma_finite M2 M1 ..
   from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
   show ?thesis by auto
 qed
 
 lemma (in pair_sigma_finite) integral_product_swap:

   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
   shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
     and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
     and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
 proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
+  interpret Q: pair_sigma_finite M2 M1 ..
   have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
     using f unfolding integrable_product_swap_iff[symmetric] by simp
   show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
   show ?INT using Q.integrable_fst'[OF Q_int] by simp
   show ?EQ using Q.integral_fst'[OF Q_int]

   fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
   shows "integral\<^sup>L (Pi\<^sub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^sub>M J M) \<partial>Pi\<^sub>M I M)"
 proof -
-  interpret I: finite_product_sigma_finite M I by default fact
-  interpret J: finite_product_sigma_finite M J by default fact
+  interpret I: finite_product_sigma_finite M I by standard fact
+  interpret J: finite_product_sigma_finite M J by standard fact
   have "finite (I \<union> J)" using fin by auto
-  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
-  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
+  interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
+  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
   let ?M = "merge I J"
   let ?f = "\<lambda>x. f (?M x)"
   from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
     by auto
   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"

 lemma (in product_sigma_finite) product_integrable_setprod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
 proof (unfold integrable_iff_bounded, intro conjI)
-  interpret finite_product_sigma_finite M I by default fact
+  interpret finite_product_sigma_finite M I by standard fact
 
   show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
     using assms by simp
   have "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) = 
       (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ereal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"

   case (insert i I)
   then have iI: "finite (insert i I)" by auto
   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
     integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
     by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
-  interpret I: finite_product_sigma_finite M I by default fact
+  interpret I: finite_product_sigma_finite M I by standard fact
   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
     using `i \<notin> I` by (auto intro!: setprod.cong)
   show ?case
     unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
     by (simp add: * insert prod subset_insertI)