src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 66748 3efac90a11a7
parent 66447 a1f5c5c26fa6
child 66804 3f9bb52082c4