src/HOL/Probability/Binary_Product_Measure.thy
changeset 46356 48fcca8965f4
parent 45777 c36637603821
child 46731 5302e932d1e5