src/HOL/Real_Vector_Spaces.thy
changeset 69506 7d59af98af29
parent 69260 0a9688695a1b
child 69512 2b54f25e66c4