changeset 63886 685fb01256af parent 63626 44ce6b524ff3 child 64008 17a20ca86d62
```     1.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Sep 15 22:41:05 2016 +0200
1.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Sep 16 13:56:51 2016 +0200
1.3 @@ -862,15 +862,15 @@
1.4    show ?integrable
1.5      using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
1.6    have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
1.7 -  proof(rule integral_cong)
1.8 +  proof(rule Bochner_Integration.integral_cong)
1.9      fix M'
1.10      assume "M' \<in> space M"
1.11      with sets_eq_imp_space_eq[OF M] have "space M' = space N"
1.12        by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
1.13 -    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
1.14 +    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty)
1.15    qed simp
1.16    then show ?integral
1.17 -    using M * by(simp add: integral_empty)
1.18 +    using M * by(simp add: Bochner_Integration.integral_empty)
1.19  next
1.20    assume *: "space N \<noteq> {}"
1.21
1.22 @@ -1213,7 +1213,7 @@
1.23    also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
1.24      by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
1.25    finally show ?integral by(simp add: bind_nonempty''[where N=K])
1.26 -qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
1.27 +qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
1.28
1.29  lemma (in prob_space) prob_space_bind:
1.30    assumes ae: "AE x in M. prob_space (N x)"
```