# HG changeset patch
# User wenzelm
# Date 968697704 -7200
# Node ID 7a9652294fe079c39ec45baa0fd86c9c94f2a9aa
# Parent  bc2c0a26bd0461373ac39ae1f11f954fc1f538bb
tuned;

diff -r bc2c0a26bd04 -r 7a9652294fe0 INSTALL
--- a/INSTALL	Mon Sep 11 20:24:06 2000 +0200
+++ b/INSTALL	Mon Sep 11 20:41:44 2000 +0200
@@ -68,15 +68,13 @@
 as SuSE, RedHat etc.).  A typical installation procedure would be like
 this (executed as root):
 
-  rpm -i smlnj-110.0-3.i386.rpm
+  rpm -i --prefix /usr/share polyml.i386.rpm
   rpm -i --prefix /usr/share isabelle.rpm
   rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
 
 The install prefix may be changed as indicated.  By default the ML
 system is expected to be at the same directory level as Isabelle
-itself; changing this arrangement requires
-[ISABELLE_HOME]/etc/settings to be adapted manually.
-
+itself; see [ISABELLE_HOME]/etc/settings of how to change this.
 
 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
 Isabelle as platform independent sources.  Precompiled object-logics
@@ -105,7 +103,6 @@
 and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
 etc.) has already been installed properly; then proceed as follows.
 
-
 * Unpacking the archives.  After unpacking the Isabelle distribution
 archives (using tar and gzip) you are left with some directory
 IsabelleYY-X.  Basically, this may be installed anywhere --- just note
@@ -113,7 +110,6 @@
 you put the contents of IsabelleYY-X will be referred to as
 [ISABELLE_HOME] subsequently.
 
-
 * Auto configuration.  There are some minor adaptions to be made of
 the Isabelle distribution to your system environment (mostly locations
 of bash and perl).  Simply do it like this:
@@ -125,7 +121,6 @@
 may safely move the system later, without having to run ./configure
 again.
 
-
 * ML system settings and compilation.  Before actual compilation you
 have to tell Isabelle about your Standard ML system.  These settings
 reside in ./etc/settings, which may be also overridden by
@@ -141,6 +136,10 @@
 
   ./build FOL HOL
 
+Explicit make targets may be given as follows:
+
+  ./build -m HOL-Real HOL
+
 After successful compilation you are ready to run the system, see 1)
 above for more information.
 
diff -r bc2c0a26bd04 -r 7a9652294fe0 README.html
--- a/README.html	Mon Sep 11 20:24:06 2000 +0200
+++ b/README.html	Mon Sep 11 20:41:44 2000 +0200
@@ -13,16 +13,16 @@
 <h2>Version information</h2>
 
 This is the internal repository version of Isabelle.  The current line
-of development introduces many new features, while attempting to keep
-incompatibilities over Isabelle98-X at a minimum.  See the
-<tt>NEWS</tt> file in the distribution for more details.
+of Isabelle99 development introduces many new concepts, while
+attempting to keep incompatibilities over Isabelle98 at a minimum.
+See the <tt>NEWS</tt> file in the distribution for more details.
 
 
 <h2>System requirements</h2>
 
 Isabelle requires a real Unix box with sufficient resources. Fun
 starts at about 32-64 MB of free main memory (somewhat depending on
-your ML system), with several tens of MB disk space and a decent CPU.
+the ML system), with several tens of MB disk space and a decent CPU.
 Speaking by today's hardware standards, any moderate Linux box should
 give a very nice platform for Isabelle.
 
@@ -42,7 +42,7 @@
 The following ML system and platform combinations are known to work
 very well:
 <ul>
-<li> Poly/ML 3.x on Linux and Sparc/Solaris.
+<li> Poly/ML 3.x on Linux/x86 and Solaris/Sparc.
 <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
 </ul>
 
@@ -68,39 +68,33 @@
 
 <h2>Installation</h2>
 
-RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
+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 distribution.  See file <tt>INSTALL</tt> as
-distributed with Isabelle for more information.
+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>).
 
 
-<h2>User interfaces</h2>
-
-The distribution includes only a very primitive interface based on
-ordinary terminal sessions. Advanced interfaces are available from
-other sources:
+<h2>User interface</h2>
 
-<ul>
-
-<li>
-<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
-David Aspinall and others is a generic Emacs interface for proof
-assistants, including Isabelle (both for the classic and Isar
+The canonical Isabelle user interface is <a
+href="http://www.dcs.ed.ac.uk/home/proofgen/">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 General is suitable for use by pacifists and Emacs
 militants 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.
 
-<li>
-<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
-David Aspinall is an older and simpler Emacs interface for Isabelle.
-It runs under recent versions of XEmacs.
+<p>
 
-</ul>
+Proof~General may be used together with the Emacs
+<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
+X-Symbol package</a>, which provides a nice way to get proper
+mathematical symbols displayed on screen.
 
 
 <h2>Other sources of information</h2>
@@ -145,9 +139,9 @@
 <p>
 
 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
-Institut fuer Informatik<br>
-T. U. Muenchen<br>
-D-80290 Muenchen<br>
+Institut für Informatik<br>
+T. U. München<br>
+D-80290 München<br>
 Germany<br>
 <br>
 E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>