src/HOL/Probability/Regularity.thy
changeset 56212 3253aaf73a01
parent 56193 c726ecfb22b6
child 56541 0e3abadbef39
     1.1 --- a/src/HOL/Probability/Regularity.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -312,7 +312,7 @@
     1.4      case 2
     1.5      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
     1.6      also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
     1.7 -      unfolding inner by (subst INFI_ereal_cminus) force+
     1.8 +      unfolding inner by (subst INF_ereal_cminus) force+
     1.9      also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
    1.10        by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    1.11      also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
    1.12 @@ -331,7 +331,7 @@
    1.13      case 1
    1.14      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    1.15      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
    1.16 -      unfolding outer by (subst SUPR_ereal_cminus) auto
    1.17 +      unfolding outer by (subst SUP_ereal_cminus) auto
    1.18      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
    1.19        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    1.20      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"