diff -r 07371b92d382 -r b0d70cf4ed18 README.html
--- a/README.html	Wed Sep 21 11:50:20 2005 +0200
+++ b/README.html	Wed Sep 21 11:50:38 2005 +0200
@@ -21,37 +21,17 @@
 
 <h2>System requirements</h2>
 
-<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>
-
-<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>
-    <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>The following ML system and platform combinations are known to work
-very well:</p>
+<p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
+following additional software:</p>
 
 <ul>
-    <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>
+    <li>A full Standard ML Compiler (e.g. Poly/ML 4.1.x, SML/NJ 110.x).</li>
+    <li>The GNU bash shell (version 2.x).</li>
+    <li>Perl (version 5.x).</li>
+    <li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li>
+    <li>A complete LaTeX installation (e.g. teTeX 1.0) -- for document preparation.</li>
 </ul>
 
-<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.</p>
-
-<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.</p>
-
 <h2>Installation</h2>
 
 <p>Binary packages are available for Isabelle/HOL and ZF for several
@@ -118,8 +98,8 @@
 <p>
 
 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
-Institut für Informatik<br>
-Technische Universität Mnchen<br>
+Institut f&uuml;r Informatik<br>
+Technische Universit&auml;t M&uuml;nchen<br>
 Boltzmannstr. 3<br>
 D-85748 Garching<br>
 Germany<br>