src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 70019 095dce9892e8
parent 69723 9b9f203e0ba3
child 70113 c8deb8ba6d05