--- a/doc-src/Ref/defining.tex Fri May 16 15:51:11 1997 +0200
+++ b/doc-src/Ref/defining.tex Fri May 16 15:53:35 1997 +0200
@@ -689,8 +689,8 @@
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 (e.g.\
-see \texttt{HOL/ex/EindhovenMC.thy}).
+output, say for interfacing external tools like model checkers (see
+also \texttt{HOL/Modelcheck}).
\index{print modes|)}