src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 69801 a99a0f5474c5
parent 69750 7d83b0abbfd7
child 69918 eddcc7c726f3