src/HOL/Probability/Weak_Convergence.thy
changeset 79940 5e85ea359563
parent 75607 3c544d64c218