src/HOL/Topological_Spaces.thy
changeset 54002 01c8f9d3b084
parent 53946 5431e1392b14
child 54258 adfc759263ab