src/HOL/Probability/Radon_Nikodym.thy
changeset 56212 3253aaf73a01
parent 56166 9a241bc276cd
child 56409 36489d77c484
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -354,7 +354,7 @@
     1.4      from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
     1.5        by (simp cong: positive_integral_cong)
     1.6    qed
     1.7 -  from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
     1.8 +  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
     1.9    then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
    1.10    proof safe
    1.11      fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
    1.12 @@ -540,7 +540,7 @@
    1.13      by (auto intro!: SUP_least emeasure_mono)
    1.14    then have "?a \<noteq> \<infinity>" using finite_emeasure_space
    1.15      by auto
    1.16 -  from SUPR_countable_SUPR[OF Q_not_empty, of "emeasure M"]
    1.17 +  from SUP_countable_SUP [OF Q_not_empty, of "emeasure M"]
    1.18    obtain Q'' where "range Q'' \<subseteq> emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
    1.19      by auto
    1.20    then have "\<forall>i. \<exists>Q'. Q'' i = emeasure M Q' \<and> Q' \<in> ?Q" by auto