src/HOL/HahnBanach/Subspace.thy
changeset 31409 d8537ba165b5
parent 30729 461ee3e49ad3