src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
Wed, 14 Jan 2015 10:15:41 +0100 Andreas Lochbihler allow line breaks in integral notation
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Fri, 21 Nov 2014 12:11:44 +0100 Andreas Lochbihler register pmf as BNF
Mon, 17 Nov 2014 18:19:06 +0100 hoelzl add reindex rules for distr and nn_integral on count_space
Fri, 14 Nov 2014 13:18:33 +0100 hoelzl cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
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
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
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
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Fri, 30 May 2014 15:56:30 +0200 hoelzl better support for restrict_space
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
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
less more (0) tip