src/HOL/Real/HahnBanach/Bounds.thy
changeset 28402 09e4aa3ddc25
parent 27612 d3eb431db035
child 29043 409d1ca929b5