src/HOL/Probability/Complete_Measure.thy
changeset 41097 a1abfa4e2b44
parent 41023 9118eb4eb8dc
child 41689 3e39b0e730d6
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Wed Dec 08 19:32:11 2010 +0100
     1.3 @@ -257,17 +257,14 @@
     1.4    show ?thesis
     1.5    proof (intro bexI)
     1.6      from AE[unfolded all_AE_countable]
     1.7 -    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
     1.8 +    show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
     1.9      proof (rule AE_mp, safe intro!: AE_cong)
    1.10        fix x assume eq: "\<forall>i. f i x = f' i x"
    1.11 -      have "g x = (SUP i. f i x)"
    1.12 -        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
    1.13 -      then show "g x = ?f x"
    1.14 -        using eq unfolding SUPR_fun_expand by auto
    1.15 +      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
    1.16 +      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
    1.17      qed
    1.18      show "?f \<in> borel_measurable M"
    1.19 -      using sf by (auto intro!: borel_measurable_SUP
    1.20 -        intro: borel_measurable_simple_function)
    1.21 +      using sf by (auto intro: borel_measurable_simple_function)
    1.22    qed
    1.23  qed
    1.24