src/HOL/Probability/Regularity.thy
changeset 56166 9a241bc276cd
parent 52141 eff000cab70f
child 56193 c726ecfb22b6
     1.1 --- a/src/HOL/Probability/Regularity.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -319,8 +319,8 @@
     1.4        by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
     1.5      also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
     1.6          (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
     1.7 -      by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
     1.8 -         (rule INF_cong, auto simp add: sU intro!: INF_cong)
     1.9 +      by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
    1.10 +        (rule INF_cong, auto simp add: sU intro!: INF_cong)
    1.11      finally have
    1.12        "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
    1.13      moreover have
    1.14 @@ -335,7 +335,7 @@
    1.15      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
    1.16        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    1.17      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
    1.18 -      by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
    1.19 +      by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
    1.20           (rule SUP_cong, auto simp: sU)
    1.21      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
    1.22      proof (safe intro!: antisym SUP_least)