src/HOL/Real_Vector_Spaces.thy
changeset 56735 9923e362789c
parent 56479 91958d4b30f7
child 56889 48a745e1bde7