src/ZF/OrderArith.thy
changeset 72847 9dda93a753b1
parent 69593 3dda49e08b9d
child 76213 e44d86131648