src/HOL/Real_Vector_Spaces.thy
changeset 59774 d1b83f7ff6fe
parent 59741 5b762cd73a8e
child 59867 58043346ca64