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