src/HOL/Probability/Borel_Space.thy
Wed, 08 Dec 2010 19:32:11 +0100 hoelzl use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
Wed, 08 Dec 2010 16:15:14 +0100 hoelzl integral over setprod
Wed, 08 Dec 2010 16:47:45 +0100 haftmann work around problems with eta-expansion of equations
Wed, 08 Dec 2010 14:52:23 +0100 haftmann nice syntax for lattice INFI, SUPR;
Mon, 06 Dec 2010 19:54:56 +0100 hoelzl folding on arbitrary Lebesgue integrable functions
Mon, 06 Dec 2010 19:54:53 +0100 hoelzl fixed spelling errors
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
Wed, 01 Dec 2010 20:12:53 +0100 hoelzl Tuned setup for borel_measurable with min, max and psuminf.
Wed, 01 Dec 2010 20:09:41 +0100 hoelzl Replace algebra_eqI by algebra.equality;
Wed, 01 Dec 2010 19:20:30 +0100 hoelzl Support product spaces on sigma finite measures.
less more (0) tip