diff -r 50a613925c4e -r cd2cd49e6c8f README.html
--- a/README.html	Wed Jun 08 23:43:19 2005 +0200
+++ b/README.html	Thu Jun 09 11:04:02 2005 +0200
@@ -15,63 +15,57 @@
 
 <h2>Version information</h2>
 
-This is the internal repository version of Isabelle.  See the
+<p>This is the internal repository version of Isabelle. See the
 <tt>NEWS</tt> file in the distribution for details on user-relevant
-changes.
-
+changes.</p>
 
 <h2>System requirements</h2>
 
-Isabelle requires a real Unix box with sufficient resources, say 64 MB
+<p>Isabelle requires a real Unix box with sufficient resources, say 64 MB
 of free main memory and a decent CPU.  Speaking by today's hardware
 standards, any moderate Linux box should give a very nice platform for
-Isabelle.
-
-<p>
+Isabelle.</p>
 
-Furthermore, Isabelle needs the following software, which is not part
-of the distribution:
+<p>Furthermore, Isabelle needs the following software, which is not part
+of the distribution:</p>
 <ul>
-<li>A full Standard ML Compiler (e.g. Poly/ML).
-<li>The GNU bash shell (version 1.x or 2.x).
-<li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
-is <em>not</em> sufficient).
+    <li>A full Standard ML Compiler (e.g. Poly/ML).</li>
+    <li>The GNU bash shell (version 1.x or 2.x).</li>
+    <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
+    is <em>not</em> sufficient).</li>
 </ul>
 
-<p>
+<p>The following ML system and platform combinations are known to work
+very well:</p>
 
-The following ML system and platform combinations are known to work
-very well:
 <ul>
-<li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
-<li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
+    <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.</li>
+    <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).</li>
 </ul>
 
-<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
+<p><a href="http://www.polyml.org/">Poly/ML</a>, previously a
 commercial product, is back in the free world.  It is by far the best
 compiler for running Isabelle, requiring the least memory and offering
-the highest performance.
+the highest performance.</p>
 
-<p> <a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more
+<p><a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more
 store and disk space, but on the other hand supports more platforms.
-The current official release is 110.
-
+The current official release is 110.</p>
 
 <h2>Installation</h2>
 
-Binary packages are available for Isabelle/HOL and ZF for several
+<p>Binary packages are available for Isabelle/HOL and ZF for several
 platforms from the Isabelle web page.  The system may be easily built
 from scratch as well, taking the traditional tar.gz source
 distribution.  See file <tt>INSTALL</tt> as distributed with Isabelle
-for more information.
+for more information.</p>
 
-Further background information may be found in the <em>Isabelle System
-Manual</em>, distributed with the sources (directory <tt>doc</tt>).
-
+<p>Further background information may be found in the <em>Isabelle System
+Manual</em>, distributed with the sources (directory <tt>doc</tt>).</p>
 
 <h2>User interface</h2>
 
-The canonical Isabelle user interface is <a
+<p>The canonical Isabelle user interface is <a
 href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall
 and others.  It is a generic (X)Emacs interface for proof assistants,
 including Isabelle (both for the classic and Isar version).  Proof
@@ -79,38 +73,31 @@
 alike. Its most prominent feature is script management, providing a
 metaphor of <em>live proof script editing</em>.  Proof General has
 recently gained a rather large following of both beginning and expert
-users of Isabelle.
+users of Isabelle.</p>
 
-<p>
-
-Proof General is distributed together with the XEmacs
+<p>Proof General is distributed together with the XEmacs
 <a href="http://x-symbol.sourceforge.net">
 X-Symbol package</a>, which provides a nice way to get proper
-mathematical symbols displayed on screen.
-
+mathematical symbols displayed on screen.</p>
 
 <h2>Other sources of information</h2>
 
 <h3>The Isabelle Page</h3>
 
-The Isabelle home page may be accessed both from Cambridge and Munich:
+<p>The Isabelle home page may be accessed both from Cambridge and Munich:</p>
 
 <ul>
-
-<li><a
-href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
-
-<li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
-
+    <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a></li>
+    <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a></li>
 </ul>
 
 
 <h3>Mailing list</h3>
 
-The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
+<p>The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
 provides a forum for Isabelle users to discuss problems and exchange
 information. To join, send a message to <a
-href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
+href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.</p>
 
 
 <h3>Personal mail</h3>
@@ -122,7 +109,7 @@
 Cambridge CB3 0FD<br>
 England<br>
 <br>
-E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
+E-mail: <a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a><br>
 Phone: +44-223-763500<br>
 Fax:   +44-223-334748<br>
 
@@ -131,13 +118,13 @@
 <p>
 
 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
-Institut fr Informatik<br>
-Technische Universit� Mnchen<br>
+Institut für Informatik<br>
+Technische Universität Mnchen<br>
 Boltzmannstr. 3<br>
 D-85748 Garching<br>
 Germany<br>
 <br>
-E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
+E-mail: <a href="mailto:nipkow@in.tum.de">nipkow@in.tum.de</a><br>
 Phone: +49-89-289-17302<br>
 Fax:   +49-89-289-17307<br>
 <p>