# HG changeset patch
# User wenzelm
# Date 941647963 -3600
# Node ID a1fb91eb9b4d3fb5816abb32654a1662e42a6ae2
# Parent  47fd71420af3f7fed45f92a4e48507d6849c2aa9
tuned;

diff -r 47fd71420af3 -r a1fb91eb9b4d src/HOL/Modelcheck/README.html
--- a/src/HOL/Modelcheck/README.html	Wed Nov 03 17:47:52 1999 +0100
+++ b/src/HOL/Modelcheck/README.html	Wed Nov 03 17:52:43 1999 +0100
@@ -18,17 +18,17 @@
 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.  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.
+model checker tactic <tt>mc_mucke_tac</tt> in action.  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 the Mucke binary
+has been installed.
 
 <p>
 
 In order to support more realistic applications, the <a
 href="http://isabelle.in.tum.de/library/HOLCF/IOA/Modelcheck">HOLCF/IOA/Modelcheck</a>
-session augments this basic mechanism by further infrastructure to
-support proofs about I/O automata.  There is a separate <a
+session augments this basic mechanism by further infrastructure for
+proofs about I/O automata.  There is a separate <a
 href="http://isabelle.in.tum.de/IOA/papers/IOA-modelcheck.pdf">paper</a>
 available, describing model checking in Isabelle/IOA in more detail.