src/HOL/Real_Vector_Spaces.thy
changeset 63325 1086d56cde86
parent 63128 24708cf4ba61
child 63469 b6900858dcb9