src/HOL/Probability/Binary_Product_Measure.thy
changeset 53453 20ff79162ff3
parent 53374 a14d2a854c02
child 54863 82acc20ded73