src/ZF/OrderArith.thy
changeset 686 be908d8d41ef
parent 437 435875e4b21d
child 753 ec86863e87c8