src/HOL/Probability/Binary_Product_Measure.thy
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 for the product measure it is enough if only one measure is sigma-finite
2012-10-11 hoelzl 2012-10-11 cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-10 hoelzl 2012-10-10 induction prove for positive_integral_fst
2012-10-10 hoelzl 2012-10-10 add induction rule for intersection-stable sigma-sets
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-12-07 hoelzl 2011-12-07 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-26 hoelzl 2011-05-26 add lemma sigma_sets_singleton
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-03-29 hoelzl 2011-03-29 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure