src/HOL/Real_Vector_Spaces.thy
changeset 68648 371e814af6f0
parent 68615 3ed4ff0b7ac4
child 68669 7ddf297cfcde