tuned;

--- a/Admin/page/index.html	Mon Nov 02 22:18:35 1998 +0100
+++ b/Admin/page/index.html	Tue Nov 03 09:47:49 1998 +0100
@@ -16,7 +16,7 @@
 environment developed at Cambridge University (<a
 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
-The latest version is <strong>Isabelle98-1</strong>. It is available
+The latest version is <strong>Isabelle98-1</strong>, it is available
 from several <a href="dist/">mirror sites</a>.
 
 <p>
@@ -48,8 +48,8 @@
 
 <dt><a
 href="http://www.in.tum.de/~isabelle/library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
-provides basic classical and intuitionistic first-order (polymorphic)
-logic.
+provides basic classical and intuitionistic first-order logic
+(polymorphic).
 
 <dt><a
 href="http://www.in.tum.de/~isabelle/library/ZF/"><strong>Isabelle/ZF</strong></a><dd>
@@ -72,11 +72,11 @@
 Isabelle/ZF provides another starting point for applications, with a
 slightly less developed library, though.  Its definitional packages
 are similar to those of Isabelle/HOL.  Untyped ZF provides more
-advanced constructions for sets than simply typed HOL.
+advanced constructions for sets than simply-typed HOL.
 
 <p>
 
-There are also a few minor object logics that may serve as further
+There are a few minor object logics that may serve as further
 examples: <a
 href="http://www.in.tum.de/~isabelle/library/CTT/">CTT</a> is an
 extensional version of Martin-L&ouml;f's Type Theory, <a
@@ -84,7 +84,7 @@
 Barendregt's Lambda Cube.  There are also some sequent calculus
 examples under <a
 href="http://www.in.tum.de/~isabelle/library/Sequents/">Sequents</a>,
-including modal or linear logics.  Again see the <a
+including modal and linear logics.  Again see the <a
 href="http://www.in.tum.de/~isabelle/library/">Isabelle theory
 library</a> for other examples.
 
@@ -113,7 +113,7 @@
 
 </ol>
 
-The first 3 steps above are fully declarative and involve no ML
+The first three steps above are fully declarative and involve no ML
 programming at all.  Thus one already gets a decent deductive
 environment based on primitive inferences (by employing the built-in
 mechanisms of Isabelle/Pure, in particular higher-order unification