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