src/HOL/Real_Vector_Spaces.thy
changeset 60986 077f663b6c24
parent 60800 7d04351c795a
child 61070 b72a990adfe2