src/HOL/Probability/Probability_Measure.thy

 proof -
   interpret finite_measure M
   proof
     show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 
   qed
-  show "prob_space M" by default fact
+  show "prob_space M" by standard fact
 qed
 
 lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
   unfolding prob_space_def finite_measure_def by simp
 

   shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f"
   unfolding distributed_def
 proof safe
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
-  interpret ST: pair_sigma_finite S T by default
+  interpret ST: pair_sigma_finite S T ..
 
   from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
   let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
   let ?P = "S \<Otimes>\<^sub>M T"
   show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")

   assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   shows "distributed M (T \<Otimes>\<^sub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"
 proof -
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
-  interpret ST: pair_sigma_finite S T by default
-  interpret TS: pair_sigma_finite T S by default
+  interpret ST: pair_sigma_finite S T ..
+  interpret TS: pair_sigma_finite T S ..
 
   note Pxy[measurable]
   show ?thesis 
     apply (subst TS.distr_pair_swap)
     unfolding distributed_def

   shows "distributed M S X Px"
   unfolding distributed_def
 proof safe
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
-  interpret ST: pair_sigma_finite S T by default
+  interpret ST: pair_sigma_finite S T ..
 
   note Pxy[measurable]
   show X: "X \<in> measurable M S" by simp
 
   show borel: "Px \<in> borel_measurable S"

   shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   unfolding distributed_def
 proof safe
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
-  interpret ST: pair_sigma_finite S T by default
+  interpret ST: pair_sigma_finite S T ..
 
   interpret X: prob_space "density S Px"
     unfolding distributed_distr_eq_density[OF X, symmetric]
     by (rule prob_space_distr) simp
   have sf_X: "sigma_finite_measure (density S Px)" ..

     using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
     by (simp add: Int_absorb2 emeasure_nonneg)
 qed
 
 lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
-  by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
+  by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
 
 lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
   assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
   shows "\<P>(x in uniform_measure M {x\<in>space M. Q x}. P x) = \<P>(x in M. P x \<bar> Q x)"
 proof cases