src/HOL/Analysis/Cartesian_Space.thy
changeset 69745 aec42cee2521
parent 69723 9b9f203e0ba3
child 69918 eddcc7c726f3