src/HOL/Analysis/Cartesian_Space.thy
changeset 70019 095dce9892e8
parent 69918 eddcc7c726f3
child 70136 f03a01a18c6e