src/HOL/Hahn_Banach/Function_Norm.thy
changeset 36550 f8da913b6c3a
parent 32960 69916a850301
child 36778 739a9379e29b