src/HOL/Real_Vector_Spaces.thy
changeset 69312 e0f68a507683
parent 69260 0a9688695a1b
child 69512 2b54f25e66c4