src/HOL/Probability/Giry_Monad.thy
2016-10-20 hoelzl 2016-10-20 HOL-Probability: move stopping time from AFP/Markov_Models
2016-10-03 hoelzl 2016-10-03 Probability: move some theorems from AFP/Density_Compiler
2016-09-30 hoelzl 2016-09-30 HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-08-05 hoelzl 2016-08-05 move measure theory from HOL-Probability to HOL-Multivariate_Analysis
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-06-16 hoelzl 2016-06-16 Probability: show that measures form a complete lattice
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-14 hoelzl 2016-04-14 Probability: move emeasure and nn_integral from ereal to ennreal
2016-01-01 wenzelm 2016-01-01 more symbols;
2015-12-17 hoelzl 2015-12-17 moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-28 wenzelm 2015-11-28 removed junk;
2015-11-11 Andreas Lochbihler 2015-11-11 add various 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-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-07 hoelzl 2015-10-07 cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-04-14 Andreas Lochbihler 2015-04-14 lemmas about integrals over bind and join on measures
2015-04-08 wenzelm 2015-04-08 eliminated suspicious Unicode character;
2015-03-23 hoelzl 2015-03-23 add measurable_submarkov
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-19 haftmann 2015-02-19 more canonical order of subscriptions avoids superfluous facts
2015-02-11 Andreas Lochbihler 2015-02-11 more lemmas
2015-01-23 Andreas Lochbihler 2015-01-23 generalise lemma
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2014-12-05 hoelzl 2014-12-05 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
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-10-07 hoelzl 2014-10-07 fix document generation for HOL-Probability
2014-10-07 hoelzl 2014-10-07 add Giry monad