The sections that follow list all the definitions and theorems in the
\ml{string} library. When the library is loaded, all the non-definitional
theorems in the library are set up to autoload when their names are mentioned
in \ML.  The definitions, however, do not autoload, since they are of very
limited utility to the user.  For convenience, definitions and theorems are
listed separately.  The name of the theory in which each theorem is stored is
given in parentheses after the name of the theorem.