src/HOL/Real_Vector_Spaces.thy
changeset 65371 ce09e947c1d5
parent 65036 ab7e11730ad8
child 65578 e4997c181cce