src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 75866 9eeed5c424f9
parent 75078 ec86cb2418e1
child 77943 ffdad62bc235