src/HOL/Real_Vector_Spaces.thy
changeset 59692 03aa1b63af10
parent 59658 0cc388370041
child 59741 5b762cd73a8e