src/HOL/Probability/Binary_Product_Measure.thy
changeset 48285 902ab51dd12a
parent 47694 05663f75964c
child 49776 199d1d5bb17e