src/HOL/Real_Vector_Spaces.thy
changeset 79400 0824ca1f1da0
parent 78656 4da1e18a9633
child 79945 ca004ccf2352
equal deleted inserted replaced
79399:11b53e039f6f 79400:0824ca1f1da0