src/HOL/Real_Vector_Spaces.thy
changeset 63183 4d04e14d7ab8
parent 63128 24708cf4ba61
child 63469 b6900858dcb9
equal deleted inserted replaced
63182:b065b4833092 63183:4d04e14d7ab8