src/HOL/HahnBanach/HahnBanachSupLemmas.thy
changeset 30549 d2d7874648bd
parent 29252 ea97aa6aeba2