src/HOL/Probability/Binary_Product_Measure.thy
Wed, 04 Nov 2015 08:13:49 +0100 ballarin Qualifiers in locale expressions default to mandatory regardless of the command.
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Thu, 16 Jul 2015 10:48:20 +0200 hoelzl move disjoint sets to their own theory
Tue, 14 Apr 2015 14:13:51 +0200 Andreas Lochbihler add lemmas
Tue, 10 Feb 2015 12:17:22 +0100 Andreas Lochbihler add another lemma to split nn_integral over product count_space
Tue, 10 Feb 2015 12:05:21 +0100 Andreas Lochbihler nn_integral can be split over arbitrary product count_spaces
Fri, 23 Jan 2015 12:04:27 +0100 hoelzl integral of the product of count spaces equals the integral of the count space of the product type
Tue, 13 Jan 2015 19:10:36 +0100 hoelzl measurability prover: removed app splitting, replaced by more powerful destruction rules
Thu, 04 Dec 2014 17:05:58 +0100 hoelzl generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Tue, 07 Oct 2014 10:34:24 +0200 hoelzl add Giry monad
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
less more (0) -15 tip