--- a/README.html Mon May 12 12:36:22 2003 +0200
+++ b/README.html Mon May 12 13:49:08 2003 +0200
@@ -49,12 +49,9 @@
compiler for running Isabelle, requiring the least memory and offering
the highest performance.
-<p> <a
-href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
-needs lots of store and disk space, but supports many more platforms.
-The current official release is 110. Basically, we still support the
-old 0.93 release, but do not recommend to use it under normal
-circumstances.
+<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> MLWorks used to be a commercial ML programming environment
developed by <a href="http://www.harlequin.com/">Harlequin</a> and was
@@ -64,10 +61,11 @@
<h2>Installation</h2>
-Binary packages are available for Isabelle/HOL and ZF on the Linux/x86
-platform. 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.
+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.
Further background information may be found in the <em>Isabelle System
Manual</em>, distributed with the sources (directory <tt>doc</tt>).
@@ -87,7 +85,7 @@
<p>
-Proof General may be used together with the Emacs
+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.