src/HOL/HahnBanach/Subspace.thy
changeset 30244 48543b307e99
parent 29252 ea97aa6aeba2
child 30729 461ee3e49ad3