src/HOL/Analysis/Euclidean_Space.thy
changeset 69554 4d4aedf9e57f
parent 69516 09bb8f470959
child 69597 ff784d5a5bfb