src/HOL/Real_Vector_Spaces.thy
changeset 66497 18a6478a574c
parent 66422 2891f33ed4c8
child 66793 deabce3ccf1f