src/HOL/Real_Vector_Spaces.thy
changeset 65573 0f3fdf689bf9
parent 65036 ab7e11730ad8
child 65578 e4997c181cce