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
```