src/HOL/Probability/Information.thy

   next
     show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
     proof
       assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
       then have disj: "AE x in M. D x = 1 \<or> D x = 0"
-        using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
+        using D(1) by (auto intro!: AE_I[OF subset_refl] sets.sets_Collect)
 
       have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
         using D(1) by auto
       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"
         using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)

       also have "\<dots> = density M D A"
         using `A \<in> sets M` D by (simp add: emeasure_density)
       finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
     qed
     show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
-      using D(1) by (auto intro: sets_Collect_conj)
+      using D(1) by (auto intro: sets.sets_Collect_conj)
 
     show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
       D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
       using D(2)
     proof (eventually_elim, safe)

   shows "absolutely_continuous S (distr (S \<Otimes>\<^isub>M T) S fst)"
 proof -
   interpret sigma_finite_measure T by fact
   { fix A assume "A \<in> sets S" "emeasure S A = 0"
     moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
-      by (auto simp: space_pair_measure dest!: sets_into_space)
+      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
     ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
       by (simp add: emeasure_pair_measure_Times) }
   then show ?thesis
     unfolding absolutely_continuous_def
     apply (auto simp: null_sets_distr_iff)

   shows "absolutely_continuous T (distr (S \<Otimes>\<^isub>M T) T snd)"
 proof -
   interpret sigma_finite_measure T by fact
   { fix A assume "A \<in> sets T" "emeasure T A = 0"
     moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
-      by (auto simp: space_pair_measure dest!: sets_into_space)
+      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
     ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
       by (simp add: emeasure_pair_measure_Times) }
   then show ?thesis
     unfolding absolutely_continuous_def
     apply (auto simp: null_sets_distr_iff)

   moreover
   have "AE x in density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x)). Py (snd x) = real (RN_deriv T (distr M T Y) (snd x))"
     unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
     unfolding distributed_distr_eq_density[OF Py]
     apply (rule ST.AE_pair_measure)
-    apply (auto intro!: sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
+    apply (auto intro!: sets.sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
                         distributed_real_measurable[OF Pxy] distributed_real_AE[OF Py]
                         borel_measurable_real_of_ereal measurable_compose[OF _ borel_measurable_RN_deriv_density])
     using distributed_RN_deriv[OF Py]
     apply auto
     done