src/HOL/Probability/Binary_Product_Measure.thy
changeset 63393 c22928719e19
parent 63333 158ab2239496