src/HOL/Real_Vector_Spaces.thy
changeset 68743 91162dd89571
parent 68669 7ddf297cfcde
child 68721 53ad5c01be3f