src/HOL/Hahn_Banach/Normed_Space.thy
changeset 48101 1b9796b7ab03
parent 46867 0883804b67bb
child 56749 e96d6b38649e