src/HOL/Probability/Radon_Nikodym.thy
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Thu, 04 Sep 2014 14:02:37 +0200 hoelzl cleanup Wfrec; introduce dependent_wf/wellorder_choice
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Mon, 19 May 2014 14:26:58 +0200 hoelzl renamed positive_integral to nn_integral
Mon, 19 May 2014 13:44:13 +0200 hoelzl fixed document generation for HOL-Probability
Mon, 19 May 2014 12:04:45 +0200 hoelzl introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
Fri, 11 Apr 2014 17:11:41 +0200 nipkow made ereal_add_nonneg_nonneg a simp rule
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Mon, 16 Dec 2013 17:08:22 +0100 immler ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
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