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