src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
changeset 42795 66fcc9882784
parent 32960 69916a850301
child 44190 fe5504984937
equal deleted inserted replaced
42794:07155da3b2f4 42795:66fcc9882784