src/HOL/Probability/Regularity.thy
changeset 50244 de72bbe42190
parent 50125 4319691be975
child 50245 dea9363887a6
--- 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)