src/HOL/Hahn_Banach/Vector_Space.thy
changeset 56918 a442dc6d244d
parent 55018 2a526bd279ed
child 57512 cc97b347b301