src/HOL/Probability/Positive_Extended_Real.thy
2011-01-14 hoelzl 2011-01-14 introduced integral syntax
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-08 hoelzl 2010-12-08 integral over setprod
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals