1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 15:05:46 2010 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:47:45 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_apply[where 'c=pextreal])
     1.8 +    by (auto simp: less_SUP_iff SUPR_apply)
     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_apply)
    1.17 +    by (auto simp: INF_less_iff 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 @@ -1423,11 +1423,20 @@
    1.22      using assms by auto
    1.23  qed
    1.24  
    1.25 +lemma INFI_fun_expand:
    1.26 +  "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
    1.27 +  by (simp add: fun_eq_iff INFI_apply)
    1.28 +
    1.29 +lemma SUPR_fun_expand:
    1.30 +  "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
    1.31 +  by (simp add: fun_eq_iff SUPR_apply)
    1.32 +
    1.33  lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
    1.34    assumes "\<And>i. f i \<in> borel_measurable M"
    1.35    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
    1.36    using assms unfolding psuminf_def
    1.37 -  by (auto intro!: borel_measurable_SUP[unfolded SUPR_apply])
    1.38 +  by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
    1.39 +
    1.40  
    1.41  section "LIMSEQ is borel measurable"
    1.42  
    1.43 @@ -1456,7 +1465,7 @@
    1.44    with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
    1.45    have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
    1.46         "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
    1.47 -    unfolding SUPR_apply INFI_apply by auto
    1.48 +    unfolding SUPR_fun_expand INFI_fun_expand by auto
    1.49    note this[THEN borel_measurable_real]
    1.50    from borel_measurable_diff[OF this]
    1.51    show ?thesis unfolding * .