src/HOL/Probability/Infinite_Product_Measure.thy
changeset 42866 b0746bd57a41
parent 42865 36353d913424
child 42950 6e5c2a3c69da
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue May 17 12:24:48 2011 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue May 17 14:36:54 2011 +0200
     1.3 @@ -917,8 +917,9 @@
     1.4      with i show "A \<in> sigma_sets ?O ?G"
     1.5        by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
     1.6    qed
     1.7 -  finally show "sets (Pi\<^isub>P I M) = sets ?S"
     1.8 +  also have "\<dots> = sets ?S"
     1.9      by (simp add: sets_sigma)
    1.10 +  finally show "sets (Pi\<^isub>P I M) = sets ?S" .
    1.11  qed simp_all
    1.12  
    1.13  lemma (in product_prob_space) measurable_into_infprod_algebra: