src/HOL/Topological_Spaces.thy
changeset 77592 832139c1b268
parent 77223 607e1e345e8f
child 78093 cec875dcc59e