src/HOL/Real_Vector_Spaces.thy
changeset 64715 33d5fa0ce6e5
parent 64272 f76b6dda2e56
child 64788 19f3d4af7a7d