# HG changeset patch
# User wenzelm
# Date 863790815 -7200
# Node ID 409382c0cc881c0f3cd785bf0153ac3eec5e8599
# Parent  4bbeb1f58a23cc43d37751f51192c503c3b92388
fixed Modelchek reference;

diff -r 4bbeb1f58a23 -r 409382c0cc88 doc-src/Ref/defining.tex
--- 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|)}