src/HOL/Hahn_Banach/Function_Order.thy
changeset 78659 b5f3d1051b13
parent 61879 e4f9d8f094fe