src/HOL/Hahn_Banach/Vector_Space.thy
changeset 38142 c202426474c3
parent 37887 2ae085b07f2f
child 41413 64cd30d6b0b8