# HG changeset patch
# User wenzelm
# Date 864118076 -7200
# Node ID 41ad2d5077be90db36e6e45810810ef76b301390
# Parent  9190438471ea60c8dbe96c764f4accb3ba290846
index: model checkers;

diff -r 9190438471ea -r 41ad2d5077be doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Tue May 20 10:44:45 1997 +0200
+++ b/doc-src/Ref/defining.tex	Tue May 20 10:47:56 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 (see
-also \texttt{HOL/Modelcheck}).
+output, say for interfacing external tools like \rmindex{model
+  checkers} (see also \texttt{HOL/Modelcheck}).
 
 \index{print modes|)}