src/HOL/Hahn_Banach/Normed_Space.thy
changeset 54924 44373f3560c7
parent 46867 0883804b67bb
child 56749 e96d6b38649e
equal deleted inserted replaced
54923:ffed2452f5f6 54924:44373f3560c7