src/HOL/Real_Vector_Spaces.thy
changeset 63569 7e0b0db5e9ac
parent 63556 36e9732988ce
child 63680 6e1e8b5abbfa
equal deleted inserted replaced
63568:e63c8f2fbd28 63569:7e0b0db5e9ac