src/HOL/Probability/Measure_Space.thy
 changeset 56212 3253aaf73a01 parent 56193 c726ecfb22b6 child 56994 8d5e5ec1cac3
```--- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 22:11:46 2014 +0100
@@ -55,7 +55,7 @@
from this[of "Suc i"] show "f i \<le> y" by auto
qed (insert assms, simp)
ultimately show ?thesis using assms
-    by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
+    by (subst suminf_ereal_eq_SUP) (auto simp: indicator_def)
qed

lemma suminf_indicator:
@@ -375,7 +375,7 @@
by auto
ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
using A(4) f_fin f_Int_fin
-    by (subst INFI_ereal_add) (auto simp: decseq_f)
+    by (subst INF_ereal_add) (auto simp: decseq_f)
moreover {
fix n
have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
@@ -543,10 +543,10 @@
have A0: "0 \<le> emeasure M (A 0)" using A by auto

have "emeasure M (A 0) - (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n. - emeasure M (A n))"
-    by (simp add: ereal_SUPR_uminus minus_ereal_def)
+    by (simp add: ereal_SUP_uminus minus_ereal_def)
also have "\<dots> = (SUP n. emeasure M (A 0) - emeasure M (A n))"
unfolding minus_ereal_def using A0 assms