src/HOL/HahnBanach/FunctionNorm.thy
changeset 30460 c999618d225e
parent 29291 d3cc5398bad5