src/HOL/Probability/Binary_Product_Measure.thy
changeset 56272 159c07ceb18c
parent 54863 82acc20ded73
child 56993 e5366291d6aa