src/HOL/Topological_Spaces.thy
changeset 78224 d85d0d41b2bd
parent 78093 cec875dcc59e
child 78516 56a408fa2440