src/HOL/Real_Vector_Spaces.thy
changeset 55770 f2cf7f92c9ac
parent 55719 cdddd073bff8
child 56194 9ffbb4004c81