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)"