src/HOL/Hahn_Banach/Subspace.thy
changeset 61214 a00bee2dfbd1
parent 61076 bdc1e2f0a86a
child 61486 3590367b0ce9