src/HOL/Analysis/Cartesian_Space.thy
changeset 82307 f6360c0c531b
parent 81472 e43bff789ac0
child 82538 4b132ea7d575