src/HOL/Probability/Binary_Product_Measure.thy
changeset 55989 55827fc7c0dd
parent 54863 82acc20ded73
child 56993 e5366291d6aa