src/HOL/Real_Vector_Spaces.thy
changeset 55831 3a9386b32211
parent 55719 cdddd073bff8
child 56194 9ffbb4004c81