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-30 hoelzl 2014-06-30 some lemmas about the indicator function; removed lemma sums_def2
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-05-30 hoelzl 2014-05-30 better support for restrict_space
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file
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-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-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 add syntax and a.e.-rules for (conditional) probability on predicates
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 measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-04-25 hoelzl 2012-04-25 add Caratheodories theorem for semi-rings of sets
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2012-04-23 hoelzl 2012-04-23 reworked Probability theory