Major Section: ACL2-BUILT-INS
(symbol-< x y) is non-nil if and only if either the
symbol-name of the symbol x lexicographially precedes the
symbol-name of the symbol y (in the sense of string<) or
else the symbol-names are equal and the symbol-package-name of
x lexicographically precedes that of y (in the same sense).
So for example, (symbol-< 'abcd 'abce) and
(symbol-< 'acl2::abcd 'foo::abce) are true.
The guard for symbol specifies that its arguments are symbols.
To see the ACL2 definition of this function, see pf.
