src/HOL/Probability/Radon_Nikodym.thy
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Tue, 19 Jul 2011 14:38:29 +0200 hoelzl add ereal to typeclass infinity
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Mon, 27 Jun 2011 09:42:46 +0200 hoelzl move conditional expectation to its own theory file
Thu, 09 Jun 2011 14:04:34 +0200 hoelzl lemma: independence is equal to mutual information = 0
Tue, 17 May 2011 14:36:54 +0200 hoelzl the measurable sets with null measure form a ring
Tue, 22 Mar 2011 20:06:10 +0100 hoelzl standardized headers
Mon, 14 Mar 2011 14:37:49 +0100 hoelzl reworked Probability theory: measures are not type restricted to positive extended reals
Wed, 23 Feb 2011 11:40:17 +0100 hoelzl add lemma RN_deriv_vimage
Fri, 04 Feb 2011 14:16:55 +0100 hoelzl add auto support for AE_mp
Wed, 02 Feb 2011 12:34:45 +0100 hoelzl the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
Mon, 24 Jan 2011 22:29:50 +0100 hoelzl use pre-image measure, instead of image
Fri, 14 Jan 2011 14:21:48 +0100 hoelzl introduced integral syntax
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 cleanup bijectivity btw. product spaces and pairs
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
Wed, 01 Dec 2010 21:03:02 +0100 hoelzl Generalized simple_functionD and less_SUP_iff.
Wed, 01 Dec 2010 19:20:30 +0100 hoelzl Support product spaces on sigma finite measures.
Thu, 02 Sep 2010 19:51:53 +0200 hoelzl Moved lemmas to appropriate locations
Thu, 02 Sep 2010 17:12:40 +0200 hoelzl move lemmas to correct theory files
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
less more (0) tip