src/HOL/Real_Vector_Spaces.thy
changeset 79101 4e47b34fbb8e
parent 78656 4da1e18a9633
child 79945 ca004ccf2352
equal deleted inserted replaced
79100:e103e3cef3cb 79101:4e47b34fbb8e