src/HOL/Real_Vector_Spaces.thy
changeset 78888 95bbf9a576b3
parent 78656 4da1e18a9633
child 79945 ca004ccf2352
equal deleted inserted replaced
78886:b82c2f801f2c 78888:95bbf9a576b3