src/HOL/Real_Vector_Spaces.thy
changeset 82276 d22e9c5b5dc6
parent 82080 0aa2d1c132b2
child 82470 785615e37846