src/HOL/Probability/Discrete_Topology.thy
changeset 63412 def97df48390
parent 62390 842917225d56
child 63627 6ddb43c6b711