src/HOL/Hahn_Banach/Function_Order.thy
changeset 59859 f9d1442c70f3
parent 58889 5b7a9633cfa8
child 61486 3590367b0ce9
equal deleted inserted replaced
59858:890b68e1e8b6 59859:f9d1442c70f3