src/HOL/Real_Vector_Spaces.thy
changeset 52593 aedf7b01c6e4
parent 52381 63eec9cea2c7
child 53374 a14d2a854c02