src/HOL/Analysis/Cartesian_Space.thy
changeset 69729 4591221824f6
parent 69723 9b9f203e0ba3
child 69918 eddcc7c726f3