src/HOL/Topological_Spaces.thy
changeset 79207 f991d3003ec8
parent 78685 07c35dec9dac
child 79945 ca004ccf2352