# HG changeset patch
# User immler
# Date 1354012187 -3600
# Node ID de72bbe421902b25ac27b0a2bfd4cb68d70890d5
# Parent  0d97ef1d6de9e11cea65efbd3b30a84447ba1a94
qualified interpretation of sigma_algebra, to avoid name clashes

diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -22,7 +22,7 @@
       (\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
 
 lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
-  using space_closed[of A] space_closed[of B] by auto
+  using sets.space_closed[of A] sets.space_closed[of B] by auto
 
 lemma space_pair_measure:
   "space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
@@ -47,7 +47,7 @@
   assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M"
   shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
   unfolding pair_measure_def using 1 2
-  by (intro measurable_measure_of) (auto dest: sets_into_space)
+  by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
 
 lemma measurable_split_replace[measurable (raw)]:
   "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
@@ -63,7 +63,7 @@
   have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
     by auto
   also have "\<dots> \<in> sets M"
-    by (rule Int) (auto intro!: measurable_sets * f g)
+    by (rule sets.Int) (auto intro!: measurable_sets * f g)
   finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
 qed
 
@@ -79,10 +79,12 @@
   using measurable_Pair[OF assms] by simp
 
 lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
-  by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
+  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+    measurable_def)
 
 lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
-  by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
+  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+    measurable_def)
 
 lemma 
   assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)" 
@@ -122,7 +124,7 @@
   assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
 proof -
   have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
-    using A[THEN sets_into_space] by (auto simp: space_pair_measure)
+    using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
   also have "\<dots> \<in> sets M2"
     using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm)
   finally show ?thesis .
@@ -134,7 +136,7 @@
 lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1"
 proof -
   have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})"
-    using A[THEN sets_into_space] by (auto simp: space_pair_measure)
+    using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
   also have "\<dots> \<in> sets M1"
     using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm)
   finally show ?thesis .
@@ -167,11 +169,11 @@
   unfolding sets_pair_measure
 proof (induct rule: sigma_sets_induct_disjoint)
   case (compl A)
-  with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
+  with sets.sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
       (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
     unfolding sets_pair_measure[symmetric]
     by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
-  with compl top show ?case
+  with compl sets.top show ?case
     by (auto intro!: measurable_If simp: space_pair_measure)
 next
   case (union F)
@@ -189,7 +191,7 @@
   let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
   { fix i
     have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i"
-      using F sets_into_space by auto
+      using F sets.sets_into_space by auto
     let ?R = "density M (indicator (F i))"
     have "finite_measure ?R"
       using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
@@ -199,7 +201,7 @@
         = emeasure M (F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q))"
       using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
     moreover have "\<And>x. F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q) = ?C x i"
-      using sets_into_space[OF Q] by (auto simp: space_pair_measure)
+      using sets.sets_into_space[OF Q] by (auto simp: space_pair_measure)
     ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N"
       by simp }
   moreover
@@ -213,7 +215,7 @@
         by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
     qed
     also have "(\<Union>i. ?C x i) = Pair x -` Q"
-      using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
+      using F sets.sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
       by (auto simp: space_pair_measure)
     finally have "emeasure M (Pair x -` Q) = (\<Sum>i. emeasure M (?C x i))"
       by simp }
@@ -255,7 +257,7 @@
                intro!: positive_integral_cong positive_integral_indicator[symmetric])
   qed
   show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
-    using space_closed[of N] space_closed[of M] by auto
+    using sets.space_closed[of N] sets.space_closed[of M] by auto
 qed fact
 
 lemma (in sigma_finite_measure) emeasure_pair_measure_alt:
@@ -296,7 +298,7 @@
     using Q measurable_pair_swap' by (auto intro: measurable_sets)
   note M1.measurable_emeasure_Pair[OF this]
   moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) -` Q"
-    using Q[THEN sets_into_space] by (auto simp: space_pair_measure)
+    using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
   ultimately show ?thesis by simp
 qed
 
@@ -374,7 +376,7 @@
   show ?thesis
   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
     show "?E \<subseteq> Pow (space ?P)"
-      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
+      using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
     show "sets ?P = sigma_sets (space ?P) ?E"
       by (simp add: sets_pair_measure space_pair_measure)
     then show "sets ?D = sigma_sets (space ?P) ?E"
@@ -386,7 +388,7 @@
     fix X assume "X \<in> ?E"
     then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
     have "(\<lambda>(y, x). (x, y)) -` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A"
-      using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure)
+      using sets.sets_into_space[OF A] sets.sets_into_space[OF B] by (auto simp: space_pair_measure)
     with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X"
       by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr
                     measurable_pair_swap' ac_simps)
@@ -399,7 +401,7 @@
     (is "_ = ?\<nu> A")
 proof -
   have [simp]: "\<And>y. (Pair y -` ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) -` A"
-    using sets_into_space[OF A] by (auto simp: space_pair_measure)
+    using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
   show ?thesis using A
     by (subst distr_pair_swap)
        (simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']
@@ -438,7 +440,7 @@
   shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
 proof (subst AE_iff_measurable[OF _ refl])
   show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
-    by (rule sets_Collect) fact
+    by (rule sets.sets_Collect) fact
   then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
       (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
     by (simp add: M2.emeasure_pair_measure)
@@ -790,7 +792,7 @@
   show ?thesis
   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
     show "?E \<subseteq> Pow (space ?P)"
-      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
+      using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
     show "sets ?P = sigma_sets (space ?P) ?E"
       by (simp add: sets_pair_measure space_pair_measure)
     then show "sets M = sigma_sets (space ?P) ?E"
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -53,7 +53,7 @@
 
 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
@@ -180,7 +180,7 @@
 
 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"
@@ -276,7 +276,8 @@
     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:
@@ -299,7 +300,7 @@
     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:
@@ -308,7 +309,7 @@
 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:
@@ -317,7 +318,7 @@
 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:
@@ -337,7 +338,7 @@
         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
 
@@ -363,7 +364,7 @@
     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)
@@ -391,7 +392,7 @@
     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)
@@ -415,7 +416,7 @@
       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
 
@@ -427,7 +428,7 @@
   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
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -22,7 +22,7 @@
 
 lemma completion_into_space:
   "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
-  using sets_into_space by auto
+  using sets.sets_into_space by auto
 
 lemma space_completion[simp]: "space (completion M) = space M"
   unfolding completion_def using space_measure_of[OF completion_into_space] by simp
@@ -43,7 +43,7 @@
   unfolding sigma_algebra_iff2
 proof (intro conjI ballI allI impI)
   show "?A \<subseteq> Pow (space M)"
-    using sets_into_space by auto
+    using sets.sets_into_space by auto
 next
   show "{} \<in> ?A" by auto
 next
@@ -238,7 +238,7 @@
       (if x \<in> ?N then ?F undefined \<union> ?N
        else if f x = undefined then ?F (f x) \<union> ?N
        else ?F (f x) - ?N)"
-      using N(2) sets_into_space by (auto split: split_if_asm simp: null_sets_def)
+      using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
     moreover { fix y have "?F y \<union> ?N \<in> sets M"
       proof cases
         assume y: "y \<in> f`space M"
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -620,7 +620,7 @@
 
 lemma PiF_gen_subset: "{(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} \<subseteq>
     Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
-  by (auto simp: Pi'_def) (blast dest: sets_into_space)
+  by (auto simp: Pi'_def) (blast dest: sets.sets_into_space)
 
 lemma space_PiF: "space (PiF I M) = (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
   unfolding PiF_def using PiF_gen_subset by (rule space_measure_of)
@@ -757,7 +757,7 @@
       done
   qed
   also have "\<dots> \<in> sets (PiF I M)"
-    apply (intro Int countable_nat_UN subsetI, safe)
+    apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
     apply (case_tac "set (from_nat i) \<in> I")
     apply simp_all
     apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]])
@@ -807,7 +807,7 @@
   case (Union a)
   have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
     by simp
-  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
+  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
   finally show ?case .
 next
   case (Compl a)
@@ -838,10 +838,10 @@
   show "(\<lambda>x. finmap_of (J x) (f x)) -` Pi' K S \<inter> space N \<in> sets N"
     unfolding eq r
     apply (simp del: INT_simps add: )
-    apply (intro conjI impI finite_INT JN Int[OF top])
+    apply (intro conjI impI sets.finite_INT JN sets.Int[OF sets.top])
     apply simp apply assumption
     apply (subst Int_assoc[symmetric])
-    apply (rule Int)
+    apply (rule sets.Int)
     apply (intro measurable_sets[OF f] *) apply force apply assumption
     apply (intro JN)
     done
@@ -865,7 +865,7 @@
   assume "i \<in> I"
   hence "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) =
     Pi' I (\<lambda>x. if x = i then A else space (M x))"
-    using sets_into_space[OF ] `A \<in> sets (M i)` assms
+    using sets.sets_into_space[OF ] `A \<in> sets (M i)` assms
     by (auto simp: space_PiF Pi'_def)
   thus ?thesis  using assms `A \<in> sets (M i)`
     by (intro in_sets_PiFI) auto
@@ -934,7 +934,7 @@
   shows "A \<inter> B \<in> sets M" using assms
 proof -
   have "A \<inter> B = (A \<inter> space M) \<inter> B"
-    using assms sets_into_space by auto
+    using assms sets.sets_into_space by auto
   thus ?thesis using assms by auto
 qed
 
@@ -959,7 +959,7 @@
   show "A \<in> sigma_sets ?\<Omega> ?R"
   proof -
     from `I \<noteq> {}` X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})"
-      using sets_into_space
+      using sets.sets_into_space
       by (auto simp: space_PiF product_def) blast
     also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
       using X `I \<noteq> {}` assms by (intro R.finite_INT) (auto simp: space_PiF)
@@ -970,7 +970,7 @@
   then obtain i B where A: "A = {f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
     by auto
   then have "A = (\<Pi>' j \<in> I. if j = i then B else space (M j))"
-    using sets_into_space[OF A(3)]
+    using sets.sets_into_space[OF A(3)]
     apply (auto simp: Pi'_iff split: split_if_asm)
     apply blast
     done
@@ -1033,7 +1033,7 @@
       sigma_sets (space ?P) {{f \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
     using sets_PiF_single[of I M] by (simp add: space_P)
   also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)"
-  proof (safe intro!: sigma_sets_subset)
+  proof (safe intro!: sets.sigma_sets_subset)
     fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
     have "(\<lambda>x. (x)\<^isub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))"
     proof (subst measurable_iff_measure_of)
@@ -1051,7 +1051,7 @@
           using S_mono
           by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
         also have "\<dots> \<in> sets ?P"
-        proof (safe intro!: countable_UN)
+        proof (safe intro!: sets.countable_UN)
           fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
             using A S_in_E
             by (simp add: P_closed)
@@ -1072,7 +1072,7 @@
     by (simp add: P_closed)
   show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)"
     using `finite I` `I \<noteq> {}`
-    by (auto intro!: sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
+    by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
 qed
 
 lemma enumerable_sigma_fprod_algebra_sigma_eq:
@@ -1176,7 +1176,7 @@
     show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
     proof
       fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
-      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets_into_space)
+      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
       let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
       have "x = \<Union>{?x J |J. finite J}" by auto
       also have "\<dots> \<in> sets borel"
@@ -1316,7 +1316,7 @@
   have "mf (fm x) \<in> extensional J"
     by (auto simp: mf_def extensional_def compose_def)
   moreover
-  have "x \<in> extensional J" using assms sets_into_space
+  have "x \<in> extensional J" using assms sets.sets_into_space
     by (force simp: space_PiM PiE_def)
   moreover
   { fix i assume "i \<in> J"
@@ -1344,7 +1344,7 @@
   have "fm ` X = (mf) -` X \<inter> space (PiF {f ` J} (\<lambda>_. M))"
   proof safe
     fix x assume "x \<in> X"
-    with mf_fm[of x] sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
+    with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
     show "fm x \<in> space (PiF {f ` J} (\<lambda>_. M))" by (simp add: space_PiF assms)
   next
     fix y x
@@ -1396,7 +1396,7 @@
   shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
   unfolding mapmeasure_def
 proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
-  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets_into_space)
+  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
   from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^isub>M J (\<lambda>_. N)) = X"
     by (auto simp: vimage_image_eq inj_on_def)
   thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -140,7 +140,7 @@
 lemma prod_emb_Pi:
   assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
   shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
-  using assms space_closed
+  using assms sets.space_closed
   by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
 
 lemma prod_emb_id:
@@ -190,14 +190,14 @@
     by (auto simp: prod_algebra_def)
   let ?A = "\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i)"
   have A: "A = ?A"
-    unfolding A using J by (intro prod_emb_PiE sets_into_space) auto
-  show "A \<in> ?R" unfolding A using J top
+    unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
+  show "A \<in> ?R" unfolding A using J sets.top
     by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
 next
   fix A assume "A \<in> ?R"
   then obtain X where A: "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
   then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
-    by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
+    by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
   from X I show "A \<in> ?L" unfolding A
     by (auto simp: prod_algebra_def)
 qed
@@ -209,7 +209,7 @@
 
 lemma prod_algebraI_finite:
   "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
-  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
+  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
 
 lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
 proof (safe intro!: Int_stableI)
@@ -232,11 +232,11 @@
     and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
     by (auto simp: prod_algebra_def)
   from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
-    using sets_into_space by auto
+    using sets.sets_into_space by auto
   then have "A = (\<Pi>\<^isub>E i\<in>I. if i\<in>J then E i else space (M i))"
     using A J by (auto simp: prod_emb_PiE)
   moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
-    using top E by auto
+    using sets.top E by auto
   ultimately show ?thesis using that by auto
 qed
 
@@ -248,7 +248,8 @@
   from prod_algebraE[OF this] guess K F . note B = this
   have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^isub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter> 
       (if i \<in> K then F i else space (M i)))"
-    unfolding A B using A(2,3,4) A(5)[THEN sets_into_space] B(2,3,4) B(5)[THEN sets_into_space]
+    unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
+      B(5)[THEN sets.sets_into_space]
     apply (subst (1 2 3) prod_emb_PiE)
     apply (simp_all add: subset_eq PiE_Int)
     apply blast
@@ -418,14 +419,14 @@
 lemma sets_PiM_I_finite[measurable]:
   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
-  using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
+  using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto
 
 lemma measurable_component_singleton:
   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
 proof (unfold measurable_def, intro CollectI conjI ballI)
   fix A assume "A \<in> sets (M i)"
   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)"
-    using sets_into_space `i \<in> I`
+    using sets.sets_into_space `i \<in> I`
     by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
     using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
@@ -460,7 +461,7 @@
   fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
   have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
     (if j = i then space (Pi\<^isub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
-    using sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
+    using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
   also have "\<dots> \<in> sets ?P"
     using A j
     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
@@ -560,7 +561,7 @@
     fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
   next
     fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
-      by (auto simp: PiE_def dest!: sets_into_space)
+      by (auto simp: PiE_def dest!: sets.sets_into_space)
   next
     fix f assume "f \<in> space (PiM I M)"
     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
@@ -584,7 +585,7 @@
     show "positive (PiM {} M) ?\<mu>"
       by (auto simp: positive_def)
     show "countably_additive (PiM {} M) ?\<mu>"
-      by (rule countably_additiveI_finite)
+      by (rule sets.countably_additiveI_finite)
          (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
   qed (auto simp: prod_emb_def)
   also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
@@ -621,13 +622,13 @@
       emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
       by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
     also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
-      using J E[rule_format, THEN sets_into_space]
+      using J E[rule_format, THEN sets.sets_into_space]
       by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
     also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
       emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
       using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
     also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
-      using J E[rule_format, THEN sets_into_space]
+      using J E[rule_format, THEN sets.sets_into_space]
       by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
     also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
       (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
@@ -640,7 +641,7 @@
     finally show "?\<mu> ?p = \<dots>" .
 
     show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
-      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
+      using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   next
     show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
       using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
@@ -650,7 +651,7 @@
       using insert by auto
   qed (auto intro!: setprod_cong)
   with insert show ?case
-    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
+    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
 qed simp
 
 lemma (in product_sigma_finite) sigma_finite: 
@@ -750,7 +751,7 @@
     let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
     let ?X = "?g -` A \<inter> space ?B"
     have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
-      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
+      using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+
     then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
       unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
     have "emeasure ?D A = emeasure ?B ?X"
@@ -792,7 +793,7 @@
   interpret I: finite_product_sigma_finite M "{i}" by default simp
   fix A assume A: "A \<in> sets (M i)"
   moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M {i} M) = (\<Pi>\<^isub>E i\<in>{i}. A)"
-    using sets_into_space by (auto simp: space_PiM)
+    using sets.sets_into_space by (auto simp: space_PiM)
   ultimately show "emeasure (M i) A = emeasure ?D A"
     using A I.measure_times[of "\<lambda>_. A"]
     by (simp add: emeasure_distr measurable_component_singleton)
@@ -846,7 +847,7 @@
   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 insert by (auto intro!: setprod_cong)
   have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^isub>M J M)"
-    using sets_into_space insert
+    using sets.sets_into_space insert
     by (intro borel_measurable_ereal_setprod
               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
        auto
@@ -1036,7 +1037,7 @@
       sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
     using sets_PiM_single[of I M] by (simp add: space_P)
   also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
-  proof (safe intro!: sigma_sets_subset)
+  proof (safe intro!: sets.sigma_sets_subset)
     fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
     then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
       apply (subst measurable_iff_measure_of)
@@ -1059,7 +1060,7 @@
     by (simp add: P_closed)
   show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
     unfolding P_def space_PiM[symmetric]
-    by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
+    by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
 qed
 
 lemma sigma_prod_algebra_sigma_eq:
@@ -1084,7 +1085,7 @@
       sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
     using sets_PiM_single[of I M] by (simp add: space_P)
   also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
-  proof (safe intro!: sigma_sets_subset)
+  proof (safe intro!: sets.sigma_sets_subset)
     fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
     have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
     proof (subst measurable_iff_measure_of)
@@ -1104,7 +1105,7 @@
           apply (auto simp: bij_betw_def)
           done
         also have "\<dots> \<in> sets ?P"
-        proof (safe intro!: countable_UN)
+        proof (safe intro!: sets.countable_UN)
           fix xs show "(\<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
             using A S_in_E
             by (simp add: P_closed)
@@ -1125,7 +1126,7 @@
     by (simp add: P_closed)
   show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
     using `finite I`
-    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
+    by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
 qed
 
 lemma pair_measure_eq_distr_PiM:
@@ -1146,7 +1147,7 @@
   also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
     using A B by (subst B.emeasure_PiM) (auto split: bool.split)
   also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
-    using A[THEN sets_into_space] B[THEN sets_into_space]
+    using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
     by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
   finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
     using A B
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -186,11 +186,11 @@
             using G by auto
           have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
               prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
-            using A_sets sets_into_space[of _ M] X `J \<noteq> {}`
+            using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}`
             by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
           also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
-            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
-            by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
+            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space
+            by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
           finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
               prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
           moreover {
@@ -224,7 +224,7 @@
             show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
               using disj by (rule disjoint_family_on_bisimulation) auto
             show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
-              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
+              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int)
           qed
           moreover { fix k
             from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
@@ -243,7 +243,7 @@
           show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
             by (auto dest!: sums_unique)
         qed (insert F, auto)
-      qed (insert sets_into_space, auto)
+      qed (insert sets.sets_into_space, auto)
       then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
       proof (rule dynkin_system.dynkin_subset, safe)
         fix X assume "X \<in> G j"
@@ -291,7 +291,7 @@
   proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
     fix i assume "i \<in> I"
     with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
-    with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
+    with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
   qed
 qed
 
@@ -394,7 +394,7 @@
     let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)"
     assume "j \<in> J"
     from E[OF this] interpret S: sigma_algebra "space M" ?S
-      using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+      using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
 
     have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
     proof (rule sigma_sets_eqI)
@@ -416,7 +416,7 @@
   proof (rule indep_sets_sigma)
     show "indep_sets ?E J"
     proof (intro indep_setsI)
-      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: finite_INT)
+      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: sets.finite_INT)
     next
       fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K"
         and "\<forall>j\<in>K. A j \<in> ?E j"
@@ -533,7 +533,7 @@
   interpret D: dynkin_system "space M" ?D
   proof (rule dynkin_systemI)
     fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
-      using sets_into_space by auto
+      using sets.sets_into_space by auto
   next
     show "space M \<in> ?D"
       using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
@@ -546,7 +546,7 @@
     also have "\<dots> = prob X * prob (space M) - prob X * prob A"
       using A prob_space by auto
     also have "\<dots> = prob X * prob (space M - A)"
-      using X_in A sets_into_space
+      using X_in A sets.sets_into_space
       by (subst finite_measure_Diff) (auto simp: field_simps)
     finally show "space M - A \<in> ?D"
       using A `X \<subseteq> space M` by auto
@@ -611,14 +611,14 @@
   proof (rule sigma_eq_dynkin)
     { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
       then have "B \<subseteq> space M"
-        by induct (insert A sets_into_space[of _ M], auto) }
+        by induct (insert A sets.sets_into_space[of _ M], auto) }
     then show "?A \<subseteq> Pow (space M)" by auto
     show "Int_stable ?A"
     proof (rule Int_stableI)
       fix a assume "a \<in> ?A" then guess n .. note a = this
       fix b assume "b \<in> ?A" then guess m .. note b = this
       interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
-        using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+        using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
       have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
         by (intro sigma_sets_subseteq UN_mono) auto
       with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
@@ -644,7 +644,7 @@
   have F1: "range F \<subseteq> events"
     using F2 by (simp add: indep_events_def subset_eq)
   { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"
-      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space
+      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space
       by auto }
   show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
   proof (rule indep_sets_sigma)
@@ -659,12 +659,12 @@
   proof
     fix j
     interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
-      using order_trans[OF F1 space_closed]
+      using order_trans[OF F1 sets.space_closed]
       by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)
     have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
       by (intro decseq_SucI INT_decseq_offset UN_mono) auto
     also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
-      using order_trans[OF F1 space_closed]
+      using order_trans[OF F1 sets.space_closed]
       by (safe intro!: S.countable_INT S.countable_UN)
          (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)
     finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
@@ -688,7 +688,7 @@
     assume A: "\<forall>j\<in>J. A j \<in> F j"
     let ?A = "\<lambda>j. if j \<in> J then A j else space M"
     have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
-      using subset_trans[OF F(1) space_closed] J A
+      using subset_trans[OF F(1) sets.space_closed] J A
       by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
     also
     from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
@@ -882,7 +882,7 @@
     show "indep_vars M' X I" unfolding indep_vars_def
     proof (intro conjI indep_setsI ballI rv)
       fix i show "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events"
-        by (auto intro!: sigma_sets_subset measurable_sets rv)
+        by (auto intro!: sets.sigma_sets_subset measurable_sets rv)
     next
       fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
       assume Y': "\<forall>j\<in>J. Y' j \<in> sigma_sets (space M) {X j -` A \<inter> space M |A. A \<in> sets (M' j)}"
@@ -892,7 +892,7 @@
         from Y'[rule_format, OF this] rv[of j]
         show "\<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)"
           by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"])
-             (auto dest: measurable_space simp: sigma_sets_eq)
+             (auto dest: measurable_space simp: sets.sigma_sets_eq)
       qed
       from bchoice[OF this] obtain Y where
         Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -311,7 +311,7 @@
   next
     fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
     then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
-      by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
+      by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
     have "emb I J (Pi\<^isub>E J X) \<in> generator"
       using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
     then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
@@ -393,7 +393,7 @@
 
 lemma (in finite_product_prob_space) finite_measure_PiM_emb:
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
-  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
+  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
   by auto
 
 lemma (in product_prob_space) PiM_component:
@@ -465,7 +465,7 @@
   then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
     (if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
               else space (\<Pi>\<^isub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
-    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets_into_space)
+    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
   show "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
     unfolding * by (auto simp: A intro!: sets_Collect_single)
 qed
@@ -507,7 +507,7 @@
   shows "Pi UNIV E \<in> sets S"
 proof -
   have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
-    using E E[THEN sets_into_space]
+    using E E[THEN sets.sets_into_space]
     by (auto simp: prod_emb_def Pi_iff extensional_def) blast
   with E show ?thesis by auto
 qed
@@ -520,7 +520,7 @@
   have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
     using E by (simp add: measure_PiM_emb)
   moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
-    using E E[THEN sets_into_space]
+    using E E[THEN sets.sets_into_space]
     by (auto simp: prod_emb_def extensional_def Pi_iff) blast
   moreover have "range ?E \<subseteq> sets S"
     using E by auto
@@ -544,7 +544,7 @@
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
   let ?X = "prod_emb ?I ?M J (\<Pi>\<^isub>E j\<in>J. E j)"
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
-    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
     (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
     (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
@@ -576,7 +576,7 @@
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
   let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
-    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
     (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -183,7 +183,7 @@
     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
@@ -198,7 +198,7 @@
       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))"
@@ -383,7 +383,7 @@
   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
@@ -400,7 +400,7 @@
   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
@@ -1571,7 +1571,7 @@
     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]
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -117,7 +117,7 @@
     using assms unfolding simple_function_def
     using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
   hence "?U \<in> sets M"
-    apply (rule finite_UN)
+    apply (rule sets.finite_UN)
     using assms unfolding simple_function_def by auto
   thus "f -` S \<inter> space M \<in> sets M" unfolding * .
 qed
@@ -152,7 +152,7 @@
     (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
   show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
     using assms unfolding simple_function_def *
-    by (rule_tac finite_UN) auto
+    by (rule_tac sets.finite_UN) auto
 qed
 
 lemma simple_function_indicator[intro, simp]:
@@ -447,7 +447,7 @@
     then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
       then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
       else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
-      using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
+      using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
     have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
       unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
     show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
@@ -637,7 +637,7 @@
         using mono by (auto elim!: AE_E)
       have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
       moreover have "?S x \<in> sets M" using assms
-        by (rule_tac Int) (auto intro!: simple_functionD)
+        by (rule_tac sets.Int) (auto intro!: simple_functionD)
       ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N"
         using `N \<in> sets M` by (auto intro!: emeasure_mono)
       moreover have "0 \<le> (emeasure M) (?S x)"
@@ -683,13 +683,13 @@
   ultimately show ?thesis by (simp add: simple_integral_def)
 next
   assume "A \<noteq> space M"
-  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
+  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
   have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
   proof safe
     fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
   next
     fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
-      using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
+      using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
   next
     show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
   qed
@@ -700,7 +700,7 @@
     show "finite (f ` space M \<union> {0})"
       using assms(2) unfolding simple_function_def by auto
     show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
-      using sets_into_space[OF assms(1)] by auto
+      using sets.sets_into_space[OF assms(1)] by auto
     have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
       by (auto simp: image_iff)
     thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
@@ -721,13 +721,13 @@
   assumes "A \<in> sets M"
   shows "integral\<^isup>S M (indicator A) = emeasure M A"
 proof cases
-  assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
+  assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto
   thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
 next
   assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto
   thus ?thesis
     using simple_integral_indicator[OF assms simple_function_const[of _ 1]]
-    using sets_into_space[OF assms]
+    using sets.sets_into_space[OF assms]
     by (auto intro!: arg_cong[where f="(emeasure M)"])
 qed
 
@@ -916,7 +916,7 @@
     qed }
   note B_mono = this
 
-  note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
+  note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B]
 
   let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
   have measure_conv: "\<And>i. (emeasure M) (u -` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))"
@@ -1351,7 +1351,7 @@
     also have "\<dots> = (emeasure M) (\<Union>n. ?M n \<inter> ?A)"
     proof (safe intro!: SUP_emeasure_incseq)
       fix n show "?M n \<inter> ?A \<in> sets M"
-        using u by (auto intro!: Int)
+        using u by (auto intro!: sets.Int)
     next
       show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})"
       proof (safe intro!: incseq_SucI)
@@ -1401,8 +1401,8 @@
 
 lemma AE_iff_positive_integral: 
   "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^isup>P M (indicator {x. \<not> P x}) = 0"
-  by (subst positive_integral_0_iff_AE)
-     (auto simp: one_ereal_def zero_ereal_def sets_Collect_neg indicator_def[abs_def] measurable_If)
+  by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
+    sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
 
 lemma positive_integral_const_If:
   "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
@@ -2463,7 +2463,7 @@
 
 lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
   (AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
-  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE space_closed)
+  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
 
 lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
 proof -
@@ -2549,7 +2549,7 @@
     by (auto simp: eventually_ae_filter)
   then have *: "{x \<in> space (density M f). \<not> P x} \<subseteq> N \<union> {x\<in>space M. \<not> 0 < f x}"
     "N \<union> {x\<in>space M. \<not> 0 < f x} \<in> sets M" and ae2: "AE x in M. x \<notin> N"
-    using f by (auto simp: subset_eq intro!: sets_Collect_neg AE_not_in)
+    using f by (auto simp: subset_eq intro!: sets.sets_Collect_neg AE_not_in)
   show "AE x in density M f. P x"
     using ae2
     unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f]
@@ -2618,7 +2618,7 @@
   also have "\<dots> = (\<integral>\<^isup>+x. indicator (S \<inter> X) x \<partial>M)"
     by (auto intro!: positive_integral_cong simp: indicator_def)
   also have "\<dots> = emeasure M (S \<inter> X)"
-    using S X by (simp add: Int)
+    using S X by (simp add: sets.Int)
   finally show ?thesis .
 qed
 
@@ -2651,7 +2651,7 @@
 proof (rule measure_eqI)
   fix A assume A: "A \<in> sets ?R"
   { fix x assume "x \<in> space M"
-    with sets_into_space[OF A]
+    with sets.sets_into_space[OF A]
     have "indicator (T' -` A \<inter> space M') (T x) = (indicator A x :: ereal)"
       using T inv by (auto simp: indicator_def measurable_space) }
   with A T T' f show "emeasure ?R A = emeasure ?L A"
@@ -2777,7 +2777,7 @@
              intro!: positive_integral_cong)
   also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
     using A B
-    by (subst positive_integral_cmult_indicator) (simp_all add: Int emeasure_nonneg)
+    by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
   finally show ?thesis .
 qed
 
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -217,7 +217,7 @@
   have "s \<in> sigma_sets (space lebesgue) (range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)}))"
     using assms by (simp add: borel_eq_atLeastAtMost)
   also have "\<dots> \<subseteq> sets lebesgue"
-  proof (safe intro!: sigma_sets_subset lebesgueI)
+  proof (safe intro!: sets.sigma_sets_subset lebesgueI)
     fix n :: nat and a b :: 'a
     let ?N = "\<chi>\<chi> i. max (- real n) (a $$ i)"
     let ?P = "\<chi>\<chi> i. min (real n) (b $$ i)"
@@ -491,7 +491,7 @@
   and sets_lborel[simp]: "sets lborel = sets borel"
   and measurable_lborel1[simp]: "measurable lborel = measurable borel"
   and measurable_lborel2[simp]: "measurable A lborel = measurable A borel"
-  using sigma_sets_eq[of borel]
+  using sets.sigma_sets_eq[of borel]
   by (auto simp add: lborel_def measurable_def[abs_def])
 
 lemma emeasure_lborel[simp]: "A \<in> sets borel \<Longrightarrow> emeasure lborel A = emeasure lebesgue A"
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -449,11 +449,11 @@
 
 lemma suminf_emeasure:
   "range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
-  using countable_UN[of A UNIV M] emeasure_countably_additive[of M]
+  using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
   by (simp add: countably_additive_def)
 
 lemma emeasure_additive: "additive (sets M) (emeasure M)"
-  by (metis countably_additive_additive emeasure_positive emeasure_countably_additive)
+  by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
 
 lemma plus_emeasure:
   "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
@@ -462,16 +462,16 @@
 lemma setsum_emeasure:
   "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
     (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
-  by (metis additive_sum emeasure_positive emeasure_additive)
+  by (metis sets.additive_sum emeasure_positive emeasure_additive)
 
 lemma emeasure_mono:
   "a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b"
-  by (metis additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
+  by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
             emeasure_positive increasingD)
 
 lemma emeasure_space:
   "emeasure M A \<le> emeasure M (space M)"
-  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets_into_space top)
+  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top)
 
 lemma emeasure_compl:
   assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>"
@@ -479,7 +479,7 @@
 proof -
   from s have "0 \<le> emeasure M s" by auto
   have "emeasure M (space M) = emeasure M (s \<union> (space M - s))" using s
-    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
+    by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space)
   also have "... = emeasure M s + emeasure M (space M - s)"
     by (rule plus_emeasure[symmetric]) (auto simp add: s)
   finally have "emeasure M (space M) = emeasure M s + emeasure M (space M - s)" .
@@ -506,7 +506,8 @@
 lemma Lim_emeasure_incseq:
   "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   using emeasure_countably_additive
-  by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
+  by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
+    emeasure_additive)
 
 lemma incseq_emeasure:
   assumes "range B \<subseteq> sets M" "incseq B"
@@ -595,10 +596,10 @@
   have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)"
     unfolding UN_disjointed_eq ..
   also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))"
-    using range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
+    using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
     by (simp add:  disjoint_family_disjointed comp_def)
   also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))"
-    using range_disjointed_sets[OF assms] assms
+    using sets.range_disjointed_sets[OF assms] assms
     by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset)
   finally show ?thesis .
 qed
@@ -676,7 +677,8 @@
   let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
   have "space M = \<Omega>"
-    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
+    using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E`
+    by blast
 
   { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
     then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
@@ -724,9 +726,9 @@
     fix F assume "F \<in> sets M"
     let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
     from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
-      using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
+      using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
     have [simp, intro]: "\<And>i. ?D i \<in> sets M"
-      using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
+      using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
       by (auto simp: subset_eq)
     have "disjoint_family ?D"
       by (auto simp: disjoint_family_disjointed)
@@ -770,7 +772,7 @@
 interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
 proof (rule ring_of_setsI)
   show "null_sets M \<subseteq> Pow (space M)"
-    using sets_into_space by auto
+    using sets.sets_into_space by auto
   show "{} \<in> null_sets M"
     by auto
   fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
@@ -904,7 +906,7 @@
 
 lemma AE_iff_null_sets:
   "N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)"
-  using Int_absorb1[OF sets_into_space, of N M]
+  using Int_absorb1[OF sets.sets_into_space, of N M]
   by (subst AE_iff_null) (auto simp: Int_def[symmetric])
 
 lemma AE_not_in:
@@ -1033,7 +1035,7 @@
   have "emeasure M A = emeasure M (A - N)"
     using N A by (subst emeasure_Diff_null_set) auto
   also have "emeasure M (A - N) \<le> emeasure M (B - N)"
-    using N A B sets_into_space by (auto intro!: emeasure_mono)
+    using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
   also have "emeasure M (B - N) = emeasure M B"
     using N B by (subst emeasure_Diff_null_set) auto
   finally show ?thesis .
@@ -1062,7 +1064,7 @@
     space: "(\<Union>i. A i) = space M" and
     measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
     using sigma_finite by auto
-  note range' = range_disjointed_sets[OF range] range
+  note range' = sets.range_disjointed_sets[OF range] range
   { fix i
     have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
       using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
@@ -1400,7 +1402,7 @@
 lemma (in finite_measure) finite_measure_compl:
   assumes S: "S \<in> sets M"
   shows "measure M (space M - S) = measure M (space M) - measure M S"
-  using measure_Diff[OF _ top S sets_into_space] S by simp
+  using measure_Diff[OF _ sets.top S sets.sets_into_space] S by simp
 
 lemma (in finite_measure) finite_measure_mono_AE:
   assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M"
@@ -1497,7 +1499,7 @@
   shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
 proof -
   have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
-    using `e \<in> sets M` sets_into_space upper by blast
+    using `e \<in> sets M` sets.sets_into_space upper by blast
   hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
   also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   proof (rule finite_measure_finite_Union)
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -66,7 +66,7 @@
 proof
   assume ae: "AE x in M. x \<in> A"
   have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
-    using `A \<in> events`[THEN sets_into_space] by auto
+    using `A \<in> events`[THEN sets.sets_into_space] by auto
   with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
     by (simp add: emeasure_compl emeasure_space_1)
   then show "prob A = 1"
@@ -273,7 +273,7 @@
   assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
   shows "cond_prob M P Q = cond_prob M P' Q'"
   using P Q
-  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets_Collect_conj)
+  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
 
 
 lemma (in prob_space) joint_distribution_Times_le_fst:
@@ -476,7 +476,7 @@
   show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
     show "?E \<subseteq> Pow (space ?P)"
-      using space_closed[of S] space_closed[of T] by (auto simp: space_pair_measure)
+      using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
     show "sets ?L = sigma_sets (space ?P) ?E"
       by (simp add: sets_pair_measure space_pair_measure)
     then show "sets ?R = sigma_sets (space ?P) ?E"
@@ -529,7 +529,7 @@
       using Pxy by auto
     { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
       let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
-      from sets_into_space[OF A]
+      from sets.sets_into_space[OF A]
       have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
         emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
         by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
@@ -849,7 +849,7 @@
 proof
   show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
     using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
-    using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
+    using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
     by (simp add: Int_absorb2 emeasure_nonneg)
 qed
 
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -25,7 +25,7 @@
   show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
     using `finite J` by (auto intro!: prod_algebraI_finite)
   { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
-  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
   show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
     using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
 
@@ -44,7 +44,7 @@
   also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
     using E by (simp add: K.measure_times)
   also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
-    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
+    using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
     using X `J \<subseteq> K` apply (subst emeasure_distr)
     by (auto intro!: measurable_restrict_subset simp: space_PiM)
@@ -93,10 +93,10 @@
   shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
 proof -
   have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
-    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
+    using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
   hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
     emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
-    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
+    using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
   proof (rule emeasure_extend_measure_Pair[OF limP_def])
     show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
@@ -133,12 +133,12 @@
   then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
   with `finite J` have "X \<in> sets (limP J M P)" by simp
   have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
-    using E sets_into_space
+    using E sets.sets_into_space
     by (auto intro!: prod_emb_PiE_same_index)
   show "emeasure (limP J M P) X = emeasure (P J) X"
     unfolding X using E
     by (intro emeasure_limP assms) simp
-qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
+qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
 
 lemma emeasure_fun_emb[simp]:
   assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
@@ -155,7 +155,7 @@
   shows "X = Y"
 proof (rule injective_vimage_restrict)
   show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
-    using sets[THEN sets_into_space] by (auto simp: space_PiM)
+    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
   have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   proof
     fix i assume "i \<in> L"
@@ -219,7 +219,7 @@
       fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
         by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
     qed
-  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+  qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
 qed
 
 lemma generatorI:
@@ -317,14 +317,14 @@
     have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
       apply (rule prod_emb_injective[of "J \<union> K" I])
       apply (insert `A \<inter> B = {}` JK J K)
-      apply (simp_all add: Int prod_emb_Int)
+      apply (simp_all add: sets.Int prod_emb_Int)
       done
     have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
       using J K by simp_all
     then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
       by simp
     also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
-      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
+      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq sets.Un del: prod_emb_Un)
     also have "\<dots> = \<mu>G A + \<mu>G B"
       using J K JK_disj by (simp add: plus_emeasure[symmetric])
     finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -243,11 +243,8 @@
         assume "x \<in> K n" hence fm_in: "fm n x \<in> fm n ` B n"
           using K' by (force simp: K_def)
         show "x \<in> B n"
-          apply (rule inj_on_image_mem_iff[OF inj_on_fm _ fm_in])
-          using `x \<in> K n` K_sets J[of n] sets_into_space
-          apply (auto simp: proj_space)
-          using J[of n] sets_into_space apply auto
-          done
+          using `x \<in> K n` K_sets sets.sets_into_space J[of n]
+          by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
       qed
       def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
       have Z': "\<And>n. Z' n \<subseteq> Z n"
@@ -263,7 +260,7 @@
         proof safe
           fix y assume "y \<in> B n"
           moreover
-          hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets_into_space[of "B n" "P (J n)"]
+          hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
             by (auto simp add: proj_space proj_sets)
           assume "fm n x = fm n y"
           note inj_onD[OF inj_on_fm[OF space_borel],
@@ -314,7 +311,7 @@
         moreover have "\<mu>G (Z n - Y n) = limP (J n) (\<lambda>_. borel) P
           (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
           unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
-          by (subst \<mu>G_eq) (auto intro!: Diff)
+          by (subst \<mu>G_eq) (auto intro!: sets.Diff)
         ultimately
         have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
           using J J_mono K_sets `n \<ge> 1`
@@ -406,7 +403,7 @@
         thus "K' (Suc n) \<noteq> {}" by auto
         fix k
         assume "k \<in> K' (Suc n)"
-        with K'[of "Suc n"] sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
+        with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
         then obtain b where "k = fm (Suc n) b" by auto
         thus "domain k = domain (fm (Suc n) (y (Suc n)))"
           by (simp_all add: fm_def)
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -189,13 +189,13 @@
       fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
       from B[OF this] show "-e < ?d B" .
     next
-      show "space M - A n \<in> sets M" by (rule compl_sets) fact
+      show "space M - A n \<in> sets M" by (rule sets.compl_sets) fact
     next
       show "?d (space M) \<le> ?d (space M - A n)"
       proof (induct n)
         fix n assume "?d (space M) \<le> ?d (space M - A n)"
         also have "\<dots> \<le> ?d (space M - A (Suc n))"
-          using A_in_sets sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
+          using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
           by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq])
         finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
       qed simp
@@ -241,7 +241,7 @@
       by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
     from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
     with S have "?P (S \<inter> X) S n"
-      by (simp add: measure_restricted sets_eq Int) (metis inf_absorb2)
+      by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
     hence "\<exists>A. ?P A S n" .. }
   note Ex_P = this
   def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
@@ -309,7 +309,7 @@
       hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
       hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
       have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
-        using sets_into_space[OF `A \<in> sets M`] by auto
+        using sets.sets_into_space[OF `A \<in> sets M`] by auto
       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
         by (auto simp: indicator_def max_def)
@@ -351,7 +351,7 @@
   have y_le: "?y \<le> N (space M)" unfolding G_def
   proof (safe intro!: SUP_least)
     fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A"
-    from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> N (space M)"
+    from this[THEN bspec, OF sets.top] show "integral\<^isup>P M g \<le> N (space M)"
       by (simp cong: positive_integral_cong)
   qed
   from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this
@@ -507,7 +507,7 @@
     with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * emeasure M A0" unfolding int_f_eq_y
       using `f \<in> G`
       by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
-    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
+    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
       by (simp cong: positive_integral_cong)
     finally have "?y < integral\<^isup>P M ?f0" by simp
     moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
@@ -536,7 +536,7 @@
   let ?a = "SUP Q:?Q. emeasure M Q"
   have "{} \<in> ?Q" by auto
   then have Q_not_empty: "?Q \<noteq> {}" by blast
-  have "?a \<le> emeasure M (space M)" using sets_into_space
+  have "?a \<le> emeasure M (space M)" using sets.sets_into_space
     by (auto intro!: SUP_least emeasure_mono)
   then have "?a \<noteq> \<infinity>" using finite_emeasure_space
     by auto
@@ -601,7 +601,7 @@
         next
           assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
           with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
-            using Q' by (auto intro!: plus_emeasure countable_UN)
+            using Q' by (auto intro!: plus_emeasure sets.countable_UN)
           also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
           proof (rule SUP_emeasure_incseq[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
             show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
@@ -712,7 +712,7 @@
       also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
         using borel Qi Q0(1) `A \<in> sets M`
         by (subst positive_integral_add) (auto simp del: ereal_infty_mult
-            simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le)
+            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
       also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
         by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
       finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
@@ -727,7 +727,7 @@
       moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
         using Q_sets `A \<in> sets M` Q0(1) by auto
       moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
-        using `A \<in> sets M` sets_into_space Q0 by auto
+        using `A \<in> sets M` sets.sets_into_space Q0 by auto
       ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
         using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
       with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
@@ -755,7 +755,7 @@
     fix A assume "A \<in> null_sets ?MT"
     with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
       by (auto simp add: null_sets_density_iff)
-    with pos sets_into_space have "AE x in M. x \<notin> A"
+    with pos sets.sets_into_space have "AE x in M. x \<notin> A"
       by (elim eventually_elim1) (auto simp: not_le[symmetric])
     then have "A \<in> null_sets M"
       using `A \<in> sets M` by (simp add: AE_iff_null_sets)
@@ -784,7 +784,7 @@
   assume "density M f = density M g"
   with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
     by (simp add: emeasure_density[symmetric])
-  from this[THEN bspec, OF top] fin
+  from this[THEN bspec, OF sets.top] fin
   have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
       and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
@@ -898,7 +898,7 @@
   let ?f'M = "density M f'"
   { fix A assume "A \<in> sets M"
     then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
-      using pos(1) sets_into_space by (force simp: indicator_def)
+      using pos(1) sets.sets_into_space by (force simp: indicator_def)
     then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
       using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
   note h_null_sets = this
@@ -994,7 +994,7 @@
   def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
   { fix i j have "A i \<inter> Q j \<in> sets M"
     unfolding A_def using f Q
-    apply (rule_tac Int)
+    apply (rule_tac sets.Int)
     by (cases i) (auto intro: measurable_sets[OF f(1)]) }
   note A_in_sets = this
   let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
@@ -1133,12 +1133,12 @@
   note sets_eq_imp_space_eq[OF N, simp]
   have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
   { fix A assume "A \<in> sets M"
-    with inv T T' sets_into_space[OF this]
+    with inv T T' sets.sets_into_space[OF this]
     have "T -` T' -` A \<inter> T -` space M' \<inter> space M = A"
       by (auto simp: measurable_def) }
   note eq = this[simp]
   { fix A assume "A \<in> sets M"
-    with inv T T' sets_into_space[OF this]
+    with inv T T' sets.sets_into_space[OF this]
     have "(T' \<circ> T) -` A \<inter> space M = A"
       by (auto simp: measurable_def) }
   note eq2 = this[simp]
@@ -1168,7 +1168,7 @@
 
   have "N = distr N M (T' \<circ> T)"
     by (subst measure_of_of_measure[of N, symmetric])
-       (auto simp add: distr_def sigma_sets_eq intro!: measure_of_eq space_closed)
+       (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
   also have "\<dots> = distr (distr N M' T) M T'"
     using T T' by (simp add: distr_distr)
   also have "\<dots> = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -428,9 +428,9 @@
       have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
         by (subst emeasure_Diff) (auto simp: sb)
       also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
-        by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
+        by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
       also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
-        by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
+        by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
       also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
         by (intro suminf_le_pos, subst emeasure_Diff)
            (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -1026,7 +1026,7 @@
 lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
   by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
 
-interpretation sigma_algebra "space M" "sets M" for M :: "'a measure"
+interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
   using measure_space[of M] by (auto simp: measure_space_def)
 
 definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
@@ -1146,7 +1146,7 @@
 
 lemma sets_eq_imp_space_eq:
   "sets M = sets M' \<Longrightarrow> space M = space M'"
-  using top[of M] top[of M'] space_closed[of M] space_closed[of M']
+  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
   by blast
 
 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
@@ -1225,7 +1225,7 @@
   shows "f \<in> measurable M N"
 proof -
   interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
-  from B top[of N] A.top space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
+  from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
   
   { fix X assume "X \<in> sigma_sets \<Omega> A"
     then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
@@ -1237,7 +1237,7 @@
         have [simp]: "f -` \<Omega> \<inter> space M = space M"
           by (auto simp add: funcset_mem [OF f])
         then show ?case
-          by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+          by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
       next
         case (Union a)
         then show ?case
@@ -1316,7 +1316,7 @@
     using measure unfolding measurable_def by (auto split: split_if_asm)
   show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
     using `A \<in> sets M'` measure P unfolding * measurable_def
-    by (auto intro!: Un)
+    by (auto intro!: sets.Un)
 qed
 
 lemma measurable_If_set:
@@ -1348,7 +1348,7 @@
         by (simp add: set_eq_iff, safe)
            (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
       with meas show ?thesis
-        by (auto intro!: Int)
+        by (auto intro!: sets.Int)
     next
       assume i: "(LEAST j. False) \<noteq> i"
       then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
@@ -1363,7 +1363,7 @@
         by auto
     qed }
   then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
-    by (intro countable_UN) auto
+    by (intro sets.countable_UN) auto
   moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
     (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
   ultimately show ?thesis by auto
@@ -1417,7 +1417,7 @@
       by (auto dest: finite_subset)
     moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
     ultimately have "f -` X \<inter> space M \<in> sets M"
-      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
+      using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
   then show ?thesis
     unfolding measurable_def by auto
 qed
@@ -1434,7 +1434,7 @@
   have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
     by auto
   also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
-    by (auto intro!: countable_UN measurable_sets)
+    by (auto intro!: sets.countable_UN measurable_sets)
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 qed
 
@@ -1466,7 +1466,7 @@
     then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
       unfolding UNIV_bool Pow_insert Pow_empty by auto
     then have "P -` X \<inter> space M \<in> sets M"
-      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
+      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
   then show "pred M P"
     by (auto simp: measurable_def)
 qed
@@ -1714,13 +1714,13 @@
   measurable_compose_rev[measurable_dest]
   pred_sets1[measurable_dest]
   pred_sets2[measurable_dest]
-  sets_into_space[measurable_dest]
+  sets.sets_into_space[measurable_dest]
 
 declare
-  top[measurable]
-  empty_sets[measurable (raw)]
-  Un[measurable (raw)]
-  Diff[measurable (raw)]
+  sets.top[measurable]
+  sets.empty_sets[measurable (raw)]
+  sets.Un[measurable (raw)]
+  sets.Diff[measurable (raw)]
 
 declare
   measurable_count_space[measurable (raw)]
@@ -1777,7 +1777,7 @@
   shows 
     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
-  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
+  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
 
 lemma pred_intros_countable_bounded[measurable (raw)]:
   fixes X :: "'i :: countable set"
@@ -1793,7 +1793,7 @@
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
-  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
 
 lemma countable_Un_Int[measurable (raw)]:
   "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
@@ -1854,7 +1854,7 @@
   by (auto simp: Int_def conj_commute eq_commute pred_def)
 
 declare
-  Int[measurable (raw)]
+  sets.Int[measurable (raw)]
 
 lemma pred_in_If[measurable (raw)]:
   "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>