src/HOL/Probability/Infinite_Product_Measure.thy
changeset 46905 6b1c0a80a57a
parent 46898 1570b30ee040
child 47694 05663f75964c
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
     1.3 @@ -874,7 +874,7 @@
     1.4        by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
     1.5      also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
     1.6        using J M.sets_into_space
     1.7 -      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
     1.8 +      by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
     1.9      also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
    1.10        using J by (intro sigma_sets_mono') auto
    1.11      finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"