doc-src/Ref/goals.tex

 cancel \texttt{goal} or \texttt{undo} itself.  It can be repeated to
 cancel a series of commands.
 \end{ttdescription}
 
 \goodbreak
-\noindent{\it Error indications for \texttt{back}:}\par\nobreak
+\noindent{\it Error indications for {\tt back}:}\par\nobreak
 \begin{itemize}
 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
   means \texttt{back} found a non-empty branch point, but that it contained
   the same proof state as the current one.
 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}