src/HOL/Real/HahnBanach/Subspace.thy
changeset 13849 2584233cf3ef
parent 13547 bf399f3bd7dc
child 14254 342634f38451