src/HOL/Probability/Discrete_Topology.thy
changeset 50092 39898c719339
parent 50089 1badf63e5d97
child 50245 dea9363887a6