src/HOL/Real_Vector_Spaces.thy
changeset 66787 64b47495676d
parent 66422 2891f33ed4c8
child 66793 deabce3ccf1f