src/HOL/Hahn_Banach/Normed_Space.thy
changeset 54042 ad7a2cfb8cb2
parent 46867 0883804b67bb
child 56749 e96d6b38649e