src/HOL/Probability/Bochner_Integration.thy
Fri, 29 Jul 2016 20:34:07 +0200 wenzelm more accurate cong del;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Thu, 14 Apr 2016 15:48:11 +0200 hoelzl Probability: move emeasure and nn_integral from ereal to ennreal
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Mon, 22 Feb 2016 14:37:56 +0000 paulson An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
less more (0) -30 -10 -6 tip