src/HOL/Hahn_Banach/Function_Order.thy
changeset 59859 f9d1442c70f3
parent 58889 5b7a9633cfa8
child 61486 3590367b0ce9