src/HOL/Real/HahnBanach/Subspace.thy
changeset 19458 a70f1b0f09cd
parent 18689 a50587cd8414
child 19736 d8d0f8f51d69