src/HOL/Real_Vector_Spaces.thy
changeset 60299 5ae2a2e74c93
parent 60026 41d81b4a0a21
child 60155 91477b3a2d6b