src/HOL/Probability/Infinite_Product_Measure.thy
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
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;
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 measurability for nat_case and comb_seq
2012-11-16 immler 2012-11-16 renamed to more appropriate lim_P for projective limit
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-11-09 immler 2012-11-09 moved lemmas into projective_family; added header for theory Projective_Family
2012-11-09 immler 2012-11-09 removed redundant/unnecessary assumptions from projective_family
2012-11-07 immler 2012-11-07 assume probability spaces; allow empty index set
2012-11-07 immler 2012-11-07 added projective_family; generalized generator in product_prob_space to projective_family
2012-11-06 immler 2012-11-06 moved lemmas further up
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-11-02 hoelzl 2012-11-02 infinite product measure is invariant under adding prefixes
2012-10-10 hoelzl 2012-10-10 infprod generator works also with empty index set
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 merge should operate on pairs
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-04-25 hoelzl 2012-04-25 add Caratheodories theorem for semi-rings of sets
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
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-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
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