src/HOL/Probability/Sigma_Algebra.thy
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-11-25 hoelzl 2015-11-25 infix syntax for measurable set
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-23 hoelzl 2015-07-23 Measures form a CCPO
2015-07-16 hoelzl 2015-07-16 move disjoint sets to their own theory
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas about restrict_space
2015-01-16 hoelzl 2015-01-16 tuned measurability proofs
2015-01-15 hoelzl 2015-01-15 piecewise measurability using restrict_space; cleanup Borel_Space
2014-12-05 hoelzl 2014-12-05 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-12-04 hoelzl 2014-12-04 generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-07 hoelzl 2014-10-07 fix document generation for HOL-Probability
2014-10-07 hoelzl 2014-10-07 add Giry monad
2014-10-06 hoelzl 2014-10-06 add measure space for (coinductive) streams
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
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-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-30 hoelzl 2014-05-30 generalizd measurability on restricted space; rule for integrability on compact sets
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-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-11-13 hoelzl 2013-11-13 fix document generation for HOL-Probability
2013-11-12 hoelzl 2013-11-12 measure of a countable union
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-09-24 Andreas Lochbihler 2013-09-24 make measure_of total
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-04-10 hoelzl 2013-04-10 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file
2012-12-05 hoelzl 2012-12-05 Show search depth in the debug output of the measurability prover
2012-11-29 hoelzl 2012-11-29 make SML/NJ happy (give names for all fields in a record)
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-16 hoelzl 2012-11-16 more measurability rules
2012-11-06 hoelzl 2012-11-06 add support for function application to measurability prover
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-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-10 hoelzl 2012-10-10 add induction rule for intersection-stable sigma-sets
2012-10-10 hoelzl 2012-10-10 add measurable_compose
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 correct lemma name
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;