src/HOL/Real_Vector_Spaces.thy
changeset 74309 42523fbf643b
parent 74007 df976eefcba0
child 74475 409ca22dee4c