src/HOL/Hahn_Banach/Function_Norm.thy
changeset 56950 c49edf06f8e4
parent 50918 3b6417e9f73e
child 57512 cc97b347b301