src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

 
 lemma (in finite_information) positive_p_sum[simp]: "0 \<le> setsum p X"
    by (auto intro!: setsum_nonneg)
 
 sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p"
-  by default (simp add: one_ereal_def emeasure_point_measure_finite)
+  by standard (simp add: one_ereal_def emeasure_point_measure_finite)
 
 sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b
-  by default simp
+  by standard simp
 
 lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = setsum p A"
   by (auto simp: measure_point_measure)
 
 locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b

   "P = (\<lambda>(k, ms). K k * (\<Prod>i<n. M (ms ! i)))"
 
 end
 
 sublocale koepf_duermuth \<subseteq> finite_information msgs P b
-proof default
+proof
   show "finite msgs" unfolding msgs_def
     using finite_lists_length_eq[OF M.finite_space, of n]
     by auto
 
   have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI)