src/HOL/HahnBanach/HahnBanachLemmas.thy
changeset 30612 cb6421b6a18f
parent 29197 6d4cb27ed19c