src/HOL/Probability/Radon_Nikodym.thy
Wed, 20 Feb 2013 12:04:42 +0100 hoelzl split dense into inner_dense_order and no_top/no_bot
Tue, 27 Nov 2012 11:29:47 +0100 immler qualified interpretation of sigma_algebra, to avoid name clashes
Tue, 06 Nov 2012 19:18:35 +0100 hoelzl add support for function application to measurability prover
Fri, 02 Nov 2012 14:23:54 +0100 hoelzl use measurability prover
Wed, 10 Oct 2012 12:12:24 +0200 hoelzl simplified entropy_uniform
Wed, 10 Oct 2012 12:12:19 +0200 hoelzl sigma_finite_iff_density_finite does not require a positive density function
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
Tue, 28 Feb 2012 21:53:36 +0100 wenzelm avoid undeclared variables in let bindings;
Wed, 07 Dec 2011 15:10:29 +0100 hoelzl remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
Mon, 05 Dec 2011 17:33:57 +0100 hoelzl real is better supported than real_of_nat, use it in the nat => ereal coercion
Fri, 16 Sep 2011 20:08:29 +0200 noschinl remove stray "using [[simp_trace]]"
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
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