src/HOL/Real_Vector_Spaces.thy
changeset 51662 3391a493f39a
parent 51531 f415febf4234
child 51641 cd05e9fcc63d