src/HOL/Real_Vector_Spaces.thy
changeset 57086 db7c735e963d
parent 56889 48a745e1bde7
child 57275 0ddb5b755cdc