src/HOL/Hahn_Banach/Function_Norm.thy
changeset 69260 0a9688695a1b
parent 63040 eb4ddd18d635