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