src/HOL/Hahn_Banach/Subspace.thy
changeset 64990 c6a7de505796
parent 63910 e4fdf9580372
child 66453 cc19f7ca2ed6