src/HOL/Real_Vector_Spaces.thy
changeset 61134 80ac5e17772d
parent 61070 b72a990adfe2
child 61169 4de9ff3ea29a