src/HOL/Real_Vector_Spaces.thy
changeset 62611 dc7cc407c911
parent 62533 bc25f3916a99
child 62623 dbc62f86a1a9