src/HOL/Probability/Infinite_Product_Measure.thy
2011-07-05 hoelzl 2011-07-05 rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-17 hoelzl 2011-05-17 the measurable sets with null measure form a ring
2011-05-17 hoelzl 2011-05-17 add some lemmas for infinite product measure
2011-04-05 hoelzl 2011-04-05 prove measurable_into_infprod_algebra and measure_infprod
2011-03-30 hoelzl 2011-03-30 products of probability measures are probability measures
2011-03-29 hoelzl 2011-03-29 rename Probability_Space to Probability_Measure
2011-03-29 hoelzl 2011-03-29 add infinite product measure