1.1 --- a/src/HOL/Probability/Regularity.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -428,9 +428,9 @@
     1.4        have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
     1.5          by (subst emeasure_Diff) (auto simp: sb)
     1.6        also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
     1.7 -        by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
     1.8 +        by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
     1.9        also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
    1.10 -        by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
    1.11 +        by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
    1.12        also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
    1.13          by (intro suminf_le_pos, subst emeasure_Diff)
    1.14             (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)