src/HOL/Probability/Binary_Product_Measure.thy
changeset 49742 ab0949eff3ca
parent 47694 05663f75964c
child 49776 199d1d5bb17e