src/HOL/Hahn_Banach/Vector_Space.thy
changeset 38865 43c934dd4bc3
parent 37887 2ae085b07f2f
child 41413 64cd30d6b0b8