src/HOL/HahnBanach/Subspace.thy
changeset 29691 9f03b5f847cd
parent 29252 ea97aa6aeba2
child 30729 461ee3e49ad3