# HG changeset patch
# User mueller
# Date 864123271 -7200
# Node ID 067dc2d0748954088ffa0681f126159f7d5e0552
# Parent  7f783705c7a4dd0a3398d014e4791196b1a31236
added eindhoven http address

diff -r 7f783705c7a4 -r 067dc2d07489 src/HOL/Modelcheck/README.html
--- a/src/HOL/Modelcheck/README.html	Tue May 20 11:53:20 1997 +0200
+++ b/src/HOL/Modelcheck/README.html	Tue May 20 12:14:31 1997 +0200
@@ -18,7 +18,7 @@
        by the model checker simply by invoking the tactic mc_tac.
 </UL>
 
-Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">Eindhoven Model Checker</A>). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x. 
+Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">model checker binary</A>) as a Sparc SunOS4 binary which also runs under Solaris2.x, or directly from Eindhoven (<A HREF="http://www.es.ele.tue.nl/geert/research/research_index.html">model checker sources</A>), where you get the C sources and documentation.