src/HOL/Real_Vector_Spaces.thy
changeset 62979 1e527c40ae40
parent 62948 7700f467892b
child 63040 eb4ddd18d635