src/HOL/Real_Vector_Spaces.thy
changeset 59884 bbf49d7dfd6f
parent 59741 5b762cd73a8e
child 59867 58043346ca64
equal deleted inserted replaced
59883:12a89103cae6 59884:bbf49d7dfd6f