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