src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 64107 87d32aa83410
parent 63945 444eafb6e864
child 64267 b9a1486e79be