src/HOL/Topological_Spaces.thy
changeset 75008 43b3d5318d72
parent 74668 2d9d02beaf96
child 75243 a2b8394ce1f1