src/HOL/Real_Vector_Spaces.thy
changeset 56254 a2dd9200854d
parent 56194 9ffbb4004c81
child 56369 2704ca85be98