src/HOL/Probability/Probability_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
Wed, 07 Oct 2015 17:11:16 +0200 hoelzl cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sun, 06 Sep 2015 22:14:51 +0200 haftmann prefer "uncurry" as canonical name for case distinction on products in combinatorial view
Fri, 23 Jan 2015 12:37:23 +0100 Andreas Lochbihler generalise lemma
Thu, 22 Jan 2015 14:51:08 +0100 hoelzl import general thms from Density_Compiler
Wed, 14 Jan 2015 09:59:12 +0100 Andreas Lochbihler allow line breaks in probability syntax
Tue, 13 Jan 2015 19:10:36 +0100 hoelzl measurability prover: removed app splitting, replaced by more powerful destruction rules
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;
Wed, 22 Oct 2014 13:58:30 +0200 Andreas Lochbihler add print translation for probability notation \<P>
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
less more (0) -14 tip