src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 12003 c09427e5f554
parent 11701 3d51fbf81c17
child 12018 ec054019c910