src/HOL/Probability/Lebesgue_Integration.thy
```     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:27 2013 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:30 2013 +0100
1.3 @@ -297,7 +297,7 @@
1.4      qed
1.5    next
1.6      fix x show "(SUP i. ?g i x) = max 0 (u x)"
1.7 -    proof (rule ereal_SUPI)
1.8 +    proof (rule SUP_eqI)
1.9        fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
1.10          by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
1.11                                       mult_nonpos_nonneg mult_nonneg_nonneg)
1.12 @@ -2147,7 +2147,7 @@
1.13      assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
1.14      have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
1.15      also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
1.16 -      by (intro limsup_mono positive_integral_positive)
1.17 +      by (simp add: Limsup_mono  positive_integral_positive)
1.18      finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
1.19      have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
1.20        using u'
1.21 @@ -2178,11 +2178,11 @@
1.22    qed
1.23
1.24    have "liminf ?f \<le> limsup ?f"
1.25 -    by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
1.26 +    by (intro Liminf_le_Limsup trivial_limit_sequentially)
1.27    moreover
1.28    { have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
1.29      also have "\<dots> \<le> liminf ?f"
1.30 -      by (intro liminf_mono positive_integral_positive)
1.31 +      by (simp add: Liminf_mono positive_integral_positive)
1.32      finally have "0 \<le> liminf ?f" . }
1.33    ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
1.34      using `limsup ?f = 0` by auto
```