src/HOL/Probability/Lebesgue_Integration.thy
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-12 hoelzl 2013-11-12 measure of a countable union
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-03-05 hoelzl 2013-03-05 move Liminf / Limsup lemmas on complete_lattices to its own file
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-12-04 hoelzl 2012-12-04 rules for improper Lebesgue integrals (using tendsto at_top)
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-16 hoelzl 2012-11-16 rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
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-11-02 hoelzl 2012-11-02 add syntax and a.e.-rules for (conditional) probability on predicates
2012-10-10 hoelzl 2012-10-10 induction prove for positive_integral_fst
2012-10-10 hoelzl 2012-10-10 strong nonnegativ (instead of ae nn) for induction rule
2012-10-10 hoelzl 2012-10-10 induction prove for positive_integral_density
2012-10-10 hoelzl 2012-10-10 add induction rules for simple functions and for Borel measurable functions
2012-10-10 hoelzl 2012-10-10 introduce induction rules for simple functions and for Borel measurable functions
2012-10-10 hoelzl 2012-10-10 joint distribution of independent variables
2012-10-10 hoelzl 2012-10-10 remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RComplete; simplifying proof in Probability
2011-11-04 wenzelm 2011-11-04 proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-07-21 haftmann 2011-07-21 ereal is a complete_linorder instance
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-06-09 hoelzl 2011-06-09 jensens inequality
2011-05-26 hoelzl 2011-05-26 integral strong monotone; finite subadditivity for measure
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-02-23 hoelzl 2011-02-23 use measure_preserving in ..._vimage lemmas
2011-02-04 hoelzl 2011-02-04 add auto support for AE_mp
2011-02-02 hoelzl 2011-02-02 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.
2011-01-24 hoelzl 2011-01-24 use pre-image measure, instead of image
2011-01-14 hoelzl 2011-01-14 tuned formalization of subalgebra
2011-01-14 hoelzl 2011-01-14 introduced integral syntax
2010-12-08 hoelzl 2010-12-08 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
2010-12-08 hoelzl 2010-12-08 integral over setprod
2010-12-08 hoelzl 2010-12-08 cleanup bijectivity btw. product spaces and pairs
2010-12-06 hoelzl 2010-12-06 folding on arbitrary Lebesgue integrable functions
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-02 hoelzl 2010-12-02 generalized simple_functionD