src/HOL/Probability/Binary_Product_Measure.thy
changeset 43333 2bdec7f430d3
parent 42984 43864e7475df
child 43920 cedb5cb948fd