src/HOL/Topological_Spaces.thy
changeset 74926 5cd2e6e17e6f
parent 74668 2d9d02beaf96
child 75243 a2b8394ce1f1