src/HOL/Probability/Binary_Product_Measure.thy
changeset 45985 2d399a776de2
parent 45777 c36637603821
child 46731 5302e932d1e5