src/HOL/Probability/Binary_Product_Measure.thy
changeset 49811 3fc6b3289c31
parent 49800 a6678da5692c
child 49825 bb5db3d1d6dd