src/HOL/Topological_Spaces.thy
changeset 77934 01c88cf514fc
parent 77223 607e1e345e8f
child 78093 cec875dcc59e