src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 70027 94494b92d8d0
parent 69723 9b9f203e0ba3
child 70113 c8deb8ba6d05