src/HOL/Hahn_Banach/Normed_Space.thy
changeset 52244 cb15da7bd550
parent 46867 0883804b67bb
child 56749 e96d6b38649e