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.