src/HOL/Probability/Weak_Convergence.thy
changeset 67505 ceb324e34c14
parent 63952 354808e9f44b
child 69260 0a9688695a1b