src/HOL/Hahn_Banach/Function_Order.thy
changeset 59409 b7cfe12acf2e
parent 58889 5b7a9633cfa8
child 61486 3590367b0ce9
equal deleted inserted replaced
59408:63cb603b5114 59409:b7cfe12acf2e