src/HOL/Real_Vector_Spaces.thy
changeset 56065 600781e03bf6
parent 55719 cdddd073bff8
child 56194 9ffbb4004c81