src/HOL/Real_Vector_Spaces.thy
changeset 60149 9b0825a00b1a
parent 60026 41d81b4a0a21
child 60155 91477b3a2d6b
equal deleted inserted replaced
60148:f0fc2378a479 60149:9b0825a00b1a