src/HOL/Real_Vector_Spaces.thy
changeset 67543 e8b2d85e4a8b
parent 67399 eab6ce8368fa
child 67673 c8caefb20564