src/HOL/Probability/Weak_Convergence.thy
changeset 76835 8d8af7e92c5e
parent 75607 3c544d64c218