src/HOL/Probability/Positive_Extended_Real.thy
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 08 Dec 2010 16:15:14 +0100 hoelzl integral over setprod
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
less more (0) tip