The old ordering function for ACL2 ordinals.
See o< for the current new ordering function for ACL2 ordinals.
To use the old functions in termination proofs, you can do:
(include-book "ordinals/e0-ordinal" :dir :system) (set-well-founded-relation e0-ord-<)
For a more thorough discussion of these functions, see the documentation at
the end of community book