src/HOL/Probability/Borel_Space.thy

   thus ?thesis by simp
 qed
 
 lemma borel_singleton[measurable]:
   "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
-  unfolding insert_def by (rule Un) auto
+  unfolding insert_def by (rule sets.Un) auto
 
 lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
   unfolding Compl_eq_Diff_UNIV by simp
 
 lemma borel_measurable_vimage:

 
 subsection "Borel space equals sigma algebras over intervals"
 
 lemma borel_sigma_sets_subset:
   "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
-  using sigma_sets_subset[of A borel] by simp
+  using sets.sigma_sets_subset[of A borel] by simp
 
 lemma borel_eq_sigmaI1:
   fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
   assumes borel_eq: "borel = sigma UNIV X"
   assumes X: "\<And>x. x \<in> X \<Longrightarrow> x \<in> sets (sigma UNIV (range F))"

     unfolding eucl_greaterThan_eq_halfspaces[where 'a='a]
     unfolding eucl_lessThan_eq_halfspaces[where 'a='a]
     by blast
   show "S \<in> ?SIGMA"
     unfolding *
-    by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace)
+    by (safe intro!: sets.countable_UN sets.Int sets.countable_INT)
+      (auto intro!: halfspace_gt_in_halfspace)
 qed auto
 
 lemma borel_eq_halfspace_le:
   "borel = sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i \<le> a}))"
   (is "_ = ?SIGMA")

     assume "x$$i \<le> a - 1 / real (Suc n)"
     also have "\<dots> < a" by auto
     finally show "x$$i < a" .
   qed
   show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: countable_UN) auto
+    by (safe intro!: sets.countable_UN) auto
 qed auto
 
 lemma borel_eq_halfspace_ge:
   "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a \<le> x $$ i}))"
   (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
   fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
   show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
-      by (safe intro!: compl_sets) auto
+      by (safe intro!: sets.compl_sets) auto
 qed auto
 
 lemma borel_eq_halfspace_greater:
   "borel = sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. a < x $$ i}))"
   (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
   fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
   show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: compl_sets) auto
+    by (safe intro!: sets.compl_sets) auto
 qed auto
 
 lemma borel_eq_atMost:
   "borel = sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))"
   (is "_ = ?SIGMA")

         by (subst (asm) Max_le_iff) auto
       then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k"
         by (auto intro!: exI[of _ k])
     qed
     show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
-      by (safe intro!: countable_UN) auto
+      by (safe intro!: sets.countable_UN) auto
   qed (auto intro: sigma_sets_top sigma_sets.Empty)
 qed auto
 
 lemma borel_eq_greaterThan:
   "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))"

       then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> -real k < x $$ ia"
         by (auto intro!: exI[of _ k])
     qed
     finally show "{x. x$$i \<le> a} \<in> ?SIGMA"
       apply (simp only:)
-      apply (safe intro!: countable_UN Diff)
+      apply (safe intro!: sets.countable_UN sets.Diff)
       apply (auto intro: sigma_sets_top)
       done
   qed (auto intro: sigma_sets_top sigma_sets.Empty)
 qed auto
 

       then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia < real k"
         by (auto intro!: exI[of _ k])
     qed
     finally show "{x. a \<le> x$$i} \<in> ?SIGMA"
       apply (simp only:)
-      apply (safe intro!: countable_UN Diff)
+      apply (safe intro!: sets.countable_UN sets.Diff)
       apply (auto intro: sigma_sets_top)
       done
   qed (auto intro: sigma_sets_top sigma_sets.Empty)
 qed auto
 

       then have "- real k \<le> x$$i" by simp }
     then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i"
       by (auto intro!: exI[of _ k])
   qed
   show "{..a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: countable_UN)
+    by (safe intro!: sets.countable_UN)
        (auto intro!: sigma_sets_top)
 qed auto
 
 lemma borel_eq_greaterThanLessThan:
   "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))"

 proof (rule borel_eq_sigmaI1[OF borel_def])
   fix M :: "'a set" assume "M \<in> {S. open S}"
   then have "open M" by simp
   show "M \<in> ?SIGMA"
     apply (subst open_UNION[OF `open M`])
-    apply (safe intro!: countable_UN)
+    apply (safe intro!: sets.countable_UN)
     apply auto
     done
 qed auto
 
 lemma borel_eq_atLeastLessThan: