--- a/src/HOL/Modelcheck/README.html Wed Nov 03 17:40:59 1999 +0100
+++ b/src/HOL/Modelcheck/README.html Wed Nov 03 17:47:52 1999 +0100
@@ -18,7 +18,10 @@
checker (version 0.3.5 is known to work). Theory <tt>MuCalculus</tt>
provides the syntactic and oracle interfaces, while
<tt>MuckeExample1</tt> and <tt>MuckeExample2</tt> demonstrate the
-model checker tactic <tt>mc_mucke_tac</tt> at work.
+model checker tactic <tt>mc_mucke_tac</tt> at work. In order to run
+the examples yourself, you only have to point <tt>MUCKE_HOME</tt> in
+Isabelle's <tt>etc/settings</tt> to the place where Mucke binary has
+been installed.
<p>