src/HOL/Probability/Projective_Limit.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
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-07-17 immler 2013-07-17 tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-01-18 hoelzl 2013-01-18 tune prove compact_eq_totally_bounded
2013-01-14 hoelzl 2013-01-14 differentiate (cover) compactness and sequential compactness
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-22 immler 2012-11-22 eliminated finite_set_sequence with countable set
2012-11-19 hoelzl 2012-11-19 tuned: use induction rule sigma_sets_induct_disjoint
2012-11-19 hoelzl 2012-11-19 tuned FinMap
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 renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
2012-11-16 immler 2012-11-16 renamed to more appropriate lim_P for projective limit
2012-11-15 immler 2012-11-15 corrected headers
2012-11-15 immler 2012-11-15 hide constants of auxiliary type finmap
2012-11-15 immler 2012-11-15 added projective limit; proof is based on auxiliary type finmap::polish_space