src/HOL/Real_Vector_Spaces.thy
changeset 62505 9e2a65912111
parent 62397 5ae24f33d343
child 62533 bc25f3916a99