src/HOL/Probability/Measurable.thy
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-01-15 hoelzl 2015-01-15 piecewise measurability using restrict_space; cleanup Borel_Space
2015-01-13 hoelzl 2015-01-13 measurability prover: removed app splitting, replaced by more powerful destruction rules
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-24 hoelzl 2014-11-24 cleanup measurability prover
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-11 Andreas Lochbihler 2014-11-11 add del option to measurable; make measurability rules available as dynamic theorem;
2014-05-20 hoelzl 2014-05-20 add various lemmas
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-03-11 hoelzl 2014-03-11 measurable_lfp/gfp: indirection not necessary
2014-03-10 hoelzl 2014-03-10 add measurability rule for (co)inductive predicates
2013-08-16 wenzelm 2013-08-16 more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
2012-12-14 wenzelm 2012-12-14 updated some headers;
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file