# HG changeset patch
# User wenzelm
# Date 941647672 -3600
# Node ID 47fd71420af3f7fed45f92a4e48507d6849c2aa9
# Parent  612352dad48ee1a6a24e3474b325844599ccd62f
MUCKE_HOME;

diff -r 612352dad48e -r 47fd71420af3 src/HOL/Modelcheck/README.html
--- 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>