src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 21676 a45af03f6827
parent 19984 29bb4659f80a
child 22931 11cc1ccad58e