src/HOL/Hahn_Banach/Function_Order.thy
changeset 57514 bdc2c6b40bf2
parent 44887 7ca82df6e951
child 58744 c434e37f290e
equal deleted inserted replaced
57513:55b2afc5ddfc 57514:bdc2c6b40bf2