src/HOL/HahnBanach/Bounds.thy
changeset 31565 da5a5589418e
parent 29252 ea97aa6aeba2