src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
2015-05-05 hoelzl 2015-05-05 add lfp/gfp rule for nn_integral
2015-04-14 Andreas Lochbihler 2015-04-14 add lemma about monotone convergence for countable integrals over arbitrary sequences
2015-03-23 hoelzl 2015-03-23 fix parameter order of NO_MATCH
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2015-01-27 hoelzl 2015-01-27 ereal: tuned proofs concerning continuity and suprema
2015-01-23 hoelzl 2015-01-23 integral of the product of count spaces equals the integral of the count space of the product type
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2015-01-14 Andreas Lochbihler 2015-01-14 allow line breaks in integral notation
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-21 Andreas Lochbihler 2014-11-21 register pmf as BNF
2014-11-17 hoelzl 2014-11-17 add reindex rules for distr and nn_integral on count_space
2014-11-14 hoelzl 2014-11-14 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
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 add Giry monad
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 better support for restrict_space
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