The old recognizer for ACL2 ordinals.
See o-p for the current recognizer 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