src/HOL/Real/HahnBanach/LinearSpace.thy
changeset 7823 742715638a01
parent 7808 fd019ac3485f