src/HOL/Real/HahnBanach/Subspace.thy
changeset 7823 742715638a01
parent 7808 fd019ac3485f
child 7917 5e5b9813cce7