src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 69981 3dced198b9ec
parent 69723 9b9f203e0ba3
child 70113 c8deb8ba6d05