--- 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.