src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 69545 4aed40ecfb43
parent 69544 5aa5a8d6e5b5
child 69611 42cc3609fedf