src/HOL/Probability/Product_PMF.thy
changeset 74290 b2ad24b5a42c
parent 73536 5131c388a9b0
child 75455 91c16c5ad3e9