src/HOL/Real_Vector_Spaces.thy
changeset 79836 c69ae2b8987e
parent 78656 4da1e18a9633
child 79945 ca004ccf2352
equal deleted inserted replaced
79835:866d96915388 79836:c69ae2b8987e