src/HOL/Probability/Binary_Product_Measure.thy
changeset 43850 7f2cbc713344
parent 42984 43864e7475df
child 43920 cedb5cb948fd