src/HOL/Hahn_Banach/Function_Norm.thy
changeset 51448 b041137f7fe5
parent 50918 3b6417e9f73e
child 57512 cc97b347b301