src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 28402 09e4aa3ddc25
parent 27612 d3eb431db035
child 29234 60f7fb56f8cd