\DOC string_CONV

\TYPE {string_CONV : conv}

\SYNOPSIS
Axiom-scheme for character string constants.

\DESCRIBE 
The conversion {string_CONV} expects its term argument to be a non-empty ascii
character string constant (for example: {"`a`"}, {"`b`"}, {"`abc`"}).  Given
such a term, for example the term {"`abc`"}, the conversion returns a theorem
that defines this constant in terms of a shorter string:
{
   |- `abc` = STRING(ASCII F T T F F F F T)`bc`
}
\noindent where {(ASCII F T T F F F F T)} is the ascii character code for the
first character in the supplied string (in this case {`a`}).

\FAILURE
Fails if applied to a term that is not of the form shown above or if applied
to the empty string {"``"}.

\SEEALSO
string_EQ_CONV.

\ENDDOC