src/ZF/OrderArith.ML
changeset 8717 20c42415c07d
parent 8201 a81d18b0a9b1
child 9173 422968aeed49
equal deleted inserted replaced
8716:49ac76cf0d54 8717:20c42415c07d