src/HOL/Probability/Positive_Infinite_Real.thy
changeset 40968 a6fcd305f7dc
parent 40874 f5a74b17a69e