src/HOL/Topological_Spaces.thy
changeset 53172 31e24d6ff1ea
parent 52729 412c9e0381a1
child 53215 5e47c31c6f7c