src/HOL/Topological_Spaces.thy
changeset 54230 b1d955791529
parent 53946 5431e1392b14
child 54258 adfc759263ab