src/HOL/Real_Vector_Spaces.thy
changeset 63229 f951c624c1a1
parent 63128 24708cf4ba61
child 63469 b6900858dcb9