src/HOL/Probability/Measurable.thy
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