src/HOL/Real_Vector_Spaces.thy
changeset 55400 1e8dd9cd320b
parent 54890 cb892d835803
child 55719 cdddd073bff8