src/HOL/Probability/Borel_Space.thy
 changeset 41080 294956ff285b parent 41026 bea75746dc9d child 41083 c987429a1298
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
1.3 @@ -1391,7 +1391,7 @@
1.4  proof safe
1.5    fix a
1.6    have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
1.7 -    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_fun_expand[where 'c=pextreal])
1.8 +    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_apply[where 'c=pextreal])
1.9    then show "{x\<in>space M. a < ?sup x} \<in> sets M"
1.10      using assms by auto
1.11  qed
1.12 @@ -1404,7 +1404,7 @@
1.13  proof safe
1.14    fix a
1.15    have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
1.16 -    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_fun_expand)
1.17 +    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_apply)
1.18    then show "{x\<in>space M. ?inf x < a} \<in> sets M"
1.19      using assms by auto
1.20  qed
1.21 @@ -1427,7 +1427,7 @@
1.22    assumes "\<And>i. f i \<in> borel_measurable M"
1.23    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
1.24    using assms unfolding psuminf_def
1.25 -  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
1.26 +  by (auto intro!: borel_measurable_SUP[unfolded SUPR_apply])
1.27
1.28  section "LIMSEQ is borel measurable"
1.29
1.30 @@ -1456,7 +1456,7 @@
1.31    with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
1.32    have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
1.33         "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
1.34 -    unfolding SUPR_fun_expand INFI_fun_expand by auto
1.35 +    unfolding SUPR_apply INFI_apply by auto
1.36    note this[THEN borel_measurable_real]
1.37    from borel_measurable_diff[OF this]
1.38    show ?thesis unfolding * .
```