updated for Isabelle2005;

--- a/COPYRIGHT	Wed Sep 21 11:50:20 2005 +0200
+++ b/COPYRIGHT	Wed Sep 21 11:50:38 2005 +0200
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 2004,
+Copyright (c) 2005,
   University of Cambridge and
   Technische Universitaet Muenchen.
 

--- a/INSTALL	Wed Sep 21 11:50:20 2005 +0200
+++ b/INSTALL	Wed Sep 21 11:50:38 2005 +0200
@@ -17,7 +17,6 @@
 site installation of Isabelle on Linux/x86 works like this:
 
   tar -C /usr/local -xzf Isabelle.tar.gz
-  tar -C /usr/local -xzf polyml_base.tar.gz
   tar -C /usr/local -xzf polyml_x86-linux.tar.gz
   tar -C /usr/local -xzf HOL_x86-linux.tar.gz
 
@@ -27,8 +26,8 @@
 
   1) [ISABELLE_HOME]/contrib
   2) [ISABELLE_HOME]/..
+  4) /usr/local
   3) /usr/share
-  4) /usr/local
   5) /opt
 
 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
@@ -49,7 +48,7 @@
 ----------------
 
 The Isabelle.tar.gz archive already contains all Isabelle sources (and
-documentation). Precompiled object-logics are provided for
+documentation).  Precompiled object-logics are provided for
 convenience.
 
 Assuming proper configuration of the underlying ML system
@@ -60,7 +59,7 @@
 
 Special object-logic targets may be specified as follows:
 
-  [ISABELLE_HOME]/build -m HOL-Complex HOL
+  [ISABELLE_HOME]/build -m HOL-Algebra HOL
 
 
 2) User installation

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