src/HOL/HahnBanach/Bounds.thy
changeset 30031 bd786c37af84
parent 29252 ea97aa6aeba2