src/HOL/Probability/Complete_Measure.thy
changeset 42866 b0746bd57a41
parent 42146 5b52c6a9c627
child 43920 cedb5cb948fd
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Tue May 17 12:24:48 2011 +0200
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Tue May 17 14:36:54 2011 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    have "(\<Union>i. S i) \<in> sets completion" using S by auto
     1.5    from null_part[OF this] guess N' .. note N' = this
     1.6    let ?N = "(\<Union>i. N i) \<union> N'"
     1.7 -  have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
     1.8 +  have null_set: "?N \<in> null_sets" using N' UN_N by (intro nullsets.Un) auto
     1.9    have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
    1.10      using N' by auto
    1.11    also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
    1.12 @@ -212,7 +212,7 @@
    1.13    from choice[OF this] obtain N where
    1.14      N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
    1.15    let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
    1.16 -  have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
    1.17 +  have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
    1.18    show ?thesis unfolding simple_function_def
    1.19    proof (safe intro!: exI[of _ ?f'])
    1.20      have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto