src/HOL/Real_Vector_Spaces.thy
changeset 57258 67d85a8aa6cc
parent 56889 48a745e1bde7
child 57275 0ddb5b755cdc