src/HOL/Topological_Spaces.thy
changeset 60570 7ed2cde6806d
parent 60182 e1ea5a6379c9
child 60585 48fdff264eb2
equal deleted inserted replaced
60569:f2f1f6860959 60570:7ed2cde6806d