\begin{theindex}

  \item \verb+"`+$\dots$\verb+`"+ (string constants), 5--6
  \item {\ptt ``\_DEF}, 14

  \indexspace

  \item {\ptt ASCII\_11}, 2, 3, 6, 14
  \item {\ptt ascii\_Axiom}, 1--2, 14
  \item {\ptt ascii\_CASES}, 2, 14
  \item {\ptt ASCII\_DEF}, 13
  \item {\ptt ascii\_EQ\_CONV}, 3, 9
  \item {\ptt ascii\_Induct}, 2, 15
  \item {\ptt ascii\_ISO\_DEF}, 13
  \item {\ptt ascii\_TY\_DEF}, 13

  \indexspace

  \item case analysis
    \subitem on type {\tt ascii}, 2
    \subitem on type {\tt string}, 4

  \indexspace

  \item function definitions
    \subitem on type {\tt ascii}, 2
    \subitem on type {\tt string}, 4

  \indexspace

  \item {\ptt load\_string}, 8, 10

  \indexspace

  \item {\ptt NOT\_EMPTY\_STRING}, 4, 15
  \item {\ptt NOT\_STRING\_EMPTY}, 4, 15

  \indexspace

  \item string constants, 5--6
  \item {\ptt STRING\_11}, 4, 6, 15
  \item {\ptt string\_Axiom}, 3--4, 15
  \item {\ptt string\_CASES}, 4, 15
  \item {\ptt string\_CONV}, 5--6, 10
  \item {\ptt STRING\_DEF}, 13
  \item {\ptt string\_EQ\_CONV}, 6, 11
  \item {\ptt string\_Induct}, 4, 15
  \item {\ptt string\_ISO\_DEF}, 14
  \item {\ptt string\_TY\_DEF}, 14
  \item structural induction, 4

  \indexspace

  \item theorems
    \subitem about the type {\tt ascii}, 2
    \subitem about the type {\tt string}, 4

\end{theindex}
