src/HOL/Topological_Spaces.thy
changeset 80578 27e66a8323b2
parent 79945 ca004ccf2352
child 80612 e65eed943bee
equal deleted inserted replaced
80575:01edf83f6dee 80578:27e66a8323b2