src/HOL/Real_Vector_Spaces.thy
changeset 54861 00d551179872
parent 54785 4876fb408c0d
child 54863 82acc20ded73