src/HOL/Probability/Radon_Nikodym.thy
changeset 42866 b0746bd57a41
parent 42067 66c8281349ec
child 43340 60e181c4eae4
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue May 17 12:24:48 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue May 17 14:36:54 2011 +0200
     1.3 @@ -975,7 +975,7 @@
     1.4        finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" by simp }
     1.5      from this[OF borel(1) refl] this[OF borel(2) f]
     1.6      have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>} \<in> null_sets" by simp_all
     1.7 -    then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule null_sets_Un)
     1.8 +    then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule nullsets.Un)
     1.9      show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
    1.10        (Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def)
    1.11    qed