src/HOL/Real_Vector_Spaces.thy
changeset 60068 ef2123db900c
parent 60026 41d81b4a0a21
child 60155 91477b3a2d6b