src/HOL/Analysis/Cartesian_Space.thy
changeset 81177 137ea3d464be
parent 80914 d97fdabd9e2b
child 81472 e43bff789ac0
equal deleted inserted replaced
81176:c0522b2d3df6 81177:137ea3d464be