src/HOL/Hahn_Banach/Normed_Space.thy
changeset 47389 e8552cba702d
parent 46867 0883804b67bb
child 56749 e96d6b38649e