src/HOL/Hahn_Banach/Hahn_Banach.thy
changeset 57618 d762318438c3
parent 56749 e96d6b38649e
child 58622 aa99568f56de