src/ZF/OrderArith.ML
changeset 12789 459b5de466b2
parent 9907 473a6604da94