src/HOL/Real_Vector_Spaces.thy
changeset 56384 5fdcfffcc72e
parent 56369 2704ca85be98
child 56409 36489d77c484