src/HOL/Probability/Binary_Product_Measure.thy
changeset 61597 53e32a9b66b8
parent 61565 352c73a689da
child 61610 4f54d2759a0b