src/HOL/Topological_Spaces.thy
changeset 78977 c7db5b4dbace
parent 78685 07c35dec9dac
child 79945 ca004ccf2352