src/HOL/Probability/Positive_Infinite_Real.thy
changeset 39712 94b1890e4e4a
parent 39302 d7728f65b353
child 40859 de0b30e6c2d2
equal deleted inserted replaced
39711:793451df8c4e 39712:94b1890e4e4a