src/HOL/Real_Vector_Spaces.thy
changeset 56166 9a241bc276cd
parent 55719 cdddd073bff8
child 56194 9ffbb4004c81
equal deleted inserted replaced
56165:dd89ce51d2c8 56166:9a241bc276cd