src/HOL/Probability/Binary_Product_Measure.thy
changeset 43168 467d5b34e1f5
parent 42984 43864e7475df
child 43920 cedb5cb948fd