src/HOL/Real_Vector_Spaces.thy
changeset 57237 bc51864c2ac4
parent 56889 48a745e1bde7
child 57275 0ddb5b755cdc