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