src/HOL/Hahn_Banach/Function_Norm.thy
changeset 61417 e39b85325b41
parent 58889 5b7a9633cfa8
child 61486 3590367b0ce9