doc-src/Ref/defining.tex

 
 \medskip The canonical application of print modes is optional printing
 of mathematical symbols from a special screen font instead of {\sc
   ascii}. Another example is to re-use Isabelle's advanced
 $\lambda$-term printing mechanisms to generate completely different
-output, say for interfacing external tools like model checkers (see
-also \texttt{HOL/Modelcheck}).
+output, say for interfacing external tools like \rmindex{model
+  checkers} (see also \texttt{HOL/Modelcheck}).
 
 \index{print modes|)}
 
 
 \section{Ambiguity of parsed expressions} \label{sec:ambiguity}