src/ZF/OrderArith.ML
changeset 3967 edd5ff9371f8
parent 3840 e0baea4d485a
child 4091 771b1f6422a8