src/HOL/Probability/Giry_Monad.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;
Tue, 14 Apr 2015 14:14:43 +0200 Andreas Lochbihler lemmas about integrals over bind and join on measures
Wed, 08 Apr 2015 21:49:45 +0200 wenzelm eliminated suspicious Unicode character;
Mon, 23 Mar 2015 10:16:20 +0100 hoelzl add measurable_submarkov
less more (0) -10 -7 tip