src/HOL/Probability/Measure_Space.thy
 changeset 51000 c9adb50f74ad parent 50419 3177d0374701 child 51351 dd1dd470690b
```--- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -50,7 +50,7 @@
then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
by (auto simp: setsum_cases)
moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
-  proof (rule ereal_SUPI)
+  proof (rule SUP_eqI)
fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
from this[of "Suc i"] show "f i \<le> y" by auto
qed (insert assms, simp)
@@ -523,7 +523,7 @@
lemma SUP_emeasure_incseq:
assumes A: "range A \<subseteq> sets M" "incseq A"
shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
-  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
+  using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
by (simp add: LIMSEQ_unique)

lemma decseq_emeasure:
@@ -1570,7 +1570,7 @@
have "incseq (\<lambda>i. ?M (F i))"
using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
-        by (rule LIMSEQ_ereal_SUPR)
+        by (rule LIMSEQ_SUP)

moreover have "(SUP n. ?M (F n)) = \<infinity>"
proof (rule SUP_PInfty)```