# HG changeset patch
# User kleing
# Date 1052740148 -7200
# Node ID 8c2b9750628f00e090e39f43c22c305c8c3bc6a6
# Parent 13f639890266c5ff51a68c2c7f0afe1a2e8ecd8b
smlnj link update, x-symbol/PG update
diff -r 13f639890266 -r 8c2b9750628f README.html
--- 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.
- SML/NJ
-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.
+
SML/NJ needs more
+store and disk space, but on the other hand supports more platforms.
+The current official release is 110.
MLWorks used to be a commercial ML programming environment
developed by Harlequin and was
@@ -64,10 +61,11 @@
Installation
-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 INSTALL
-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 INSTALL as distributed with Isabelle
+for more information.
Further background information may be found in the Isabelle System
Manual, distributed with the sources (directory doc).
@@ -87,7 +85,7 @@
-Proof General may be used together with the Emacs
+Proof General is distributed together with the XEmacs
X-Symbol package, which provides a nice way to get proper
mathematical symbols displayed on screen.