src/HOL/Hahn_Banach/Function_Norm.thy
changeset 54230 b1d955791529
parent 50918 3b6417e9f73e
child 57512 cc97b347b301