src/HOL/Probability/Positive_Extended_Real.thy
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
less more (0) tip