src/HOL/Analysis/Cartesian_Space.thy
changeset 81177 137ea3d464be
parent 80914 d97fdabd9e2b
child 81472 e43bff789ac0