src/HOL/Hahn_Banach/Function_Norm.thy
changeset 54609 c71eb0537d37
parent 50918 3b6417e9f73e
child 57512 cc97b347b301