src/HOL/Real_Vector_Spaces.thy
changeset 63183 4d04e14d7ab8
parent 63128 24708cf4ba61
child 63469 b6900858dcb9