src/HOL/Vector_Spaces.thy
changeset 83517 d349fb17f699
parent 82802 547335b41005