src/HOL/Probability/Radon_Nikodym.thy
changeset 54776 db890d9fc5c2
parent 53374 a14d2a854c02
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -686,7 +686,7 @@
     1.4    from choice[OF this[unfolded Bex_def]]
     1.5    obtain f where borel: "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
     1.6      and f_density: "\<And>i. density (?M i) (f i) = ?N i"
     1.7 -    by auto
     1.8 +    by force
     1.9    { fix A i assume A: "A \<in> sets M"
    1.10      with Q borel have "(\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M) = emeasure (density (?M i) (f i)) A"
    1.11        by (auto simp add: emeasure_density positive_integral_density subset_eq