src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy
changeset 55018 2a526bd279ed
parent 31795 be3e1cc5005c
child 62390 842917225d56