src/HOL/HahnBanach/Subspace.thy
changeset 31794 71af1fd6a5e4
parent 30729 461ee3e49ad3