src/HOL/Topological_Spaces.thy
changeset 78852 2700e4b484f7
parent 78685 07c35dec9dac
child 79945 ca004ccf2352