src/HOL/Real_Vector_Spaces.thy
changeset 61709 47f7263870a0
parent 61649 268d88ec9087
child 61762 d50b993b4fb9