src/HOL/Probability/Discrete_Topology.thy
changeset 63056 9b95ae9ec671
parent 62390 842917225d56
child 63627 6ddb43c6b711