tuned;
authorwenzelm
Mon Sep 11 20:41:44 2000 +0200 (2000-09-11)
changeset 99277a9652294fe0
parent 9926 bc2c0a26bd04
child 9928 b7698bd95a94
tuned;
INSTALL
README.html
     1.1 --- a/INSTALL	Mon Sep 11 20:24:06 2000 +0200
     1.2 +++ b/INSTALL	Mon Sep 11 20:41:44 2000 +0200
     1.3 @@ -68,15 +68,13 @@
     1.4  as SuSE, RedHat etc.).  A typical installation procedure would be like
     1.5  this (executed as root):
     1.6  
     1.7 -  rpm -i smlnj-110.0-3.i386.rpm
     1.8 +  rpm -i --prefix /usr/share polyml.i386.rpm
     1.9    rpm -i --prefix /usr/share isabelle.rpm
    1.10    rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    1.11  
    1.12  The install prefix may be changed as indicated.  By default the ML
    1.13  system is expected to be at the same directory level as Isabelle
    1.14 -itself; changing this arrangement requires
    1.15 -[ISABELLE_HOME]/etc/settings to be adapted manually.
    1.16 -
    1.17 +itself; see [ISABELLE_HOME]/etc/settings of how to change this.
    1.18  
    1.19  Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    1.20  Isabelle as platform independent sources.  Precompiled object-logics
    1.21 @@ -105,7 +103,6 @@
    1.22  and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
    1.23  etc.) has already been installed properly; then proceed as follows.
    1.24  
    1.25 -
    1.26  * Unpacking the archives.  After unpacking the Isabelle distribution
    1.27  archives (using tar and gzip) you are left with some directory
    1.28  IsabelleYY-X.  Basically, this may be installed anywhere --- just note
    1.29 @@ -113,7 +110,6 @@
    1.30  you put the contents of IsabelleYY-X will be referred to as
    1.31  [ISABELLE_HOME] subsequently.
    1.32  
    1.33 -
    1.34  * Auto configuration.  There are some minor adaptions to be made of
    1.35  the Isabelle distribution to your system environment (mostly locations
    1.36  of bash and perl).  Simply do it like this:
    1.37 @@ -125,7 +121,6 @@
    1.38  may safely move the system later, without having to run ./configure
    1.39  again.
    1.40  
    1.41 -
    1.42  * ML system settings and compilation.  Before actual compilation you
    1.43  have to tell Isabelle about your Standard ML system.  These settings
    1.44  reside in ./etc/settings, which may be also overridden by
    1.45 @@ -141,6 +136,10 @@
    1.46  
    1.47    ./build FOL HOL
    1.48  
    1.49 +Explicit make targets may be given as follows:
    1.50 +
    1.51 +  ./build -m HOL-Real HOL
    1.52 +
    1.53  After successful compilation you are ready to run the system, see 1)
    1.54  above for more information.
    1.55  
     2.1 --- a/README.html	Mon Sep 11 20:24:06 2000 +0200
     2.2 +++ b/README.html	Mon Sep 11 20:41:44 2000 +0200
     2.3 @@ -13,16 +13,16 @@
     2.4  <h2>Version information</h2>
     2.5  
     2.6  This is the internal repository version of Isabelle.  The current line
     2.7 -of development introduces many new features, while attempting to keep
     2.8 -incompatibilities over Isabelle98-X at a minimum.  See the
     2.9 -<tt>NEWS</tt> file in the distribution for more details.
    2.10 +of Isabelle99 development introduces many new concepts, while
    2.11 +attempting to keep incompatibilities over Isabelle98 at a minimum.
    2.12 +See the <tt>NEWS</tt> file in the distribution for more details.
    2.13  
    2.14  
    2.15  <h2>System requirements</h2>
    2.16  
    2.17  Isabelle requires a real Unix box with sufficient resources. Fun
    2.18  starts at about 32-64 MB of free main memory (somewhat depending on
    2.19 -your ML system), with several tens of MB disk space and a decent CPU.
    2.20 +the ML system), with several tens of MB disk space and a decent CPU.
    2.21  Speaking by today's hardware standards, any moderate Linux box should
    2.22  give a very nice platform for Isabelle.
    2.23  
    2.24 @@ -42,7 +42,7 @@
    2.25  The following ML system and platform combinations are known to work
    2.26  very well:
    2.27  <ul>
    2.28 -<li> Poly/ML 3.x on Linux and Sparc/Solaris.
    2.29 +<li> Poly/ML 3.x on Linux/x86 and Solaris/Sparc.
    2.30  <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    2.31  </ul>
    2.32  
    2.33 @@ -68,39 +68,33 @@
    2.34  
    2.35  <h2>Installation</h2>
    2.36  
    2.37 -RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    2.38 +Binary packages are available for Isabelle/HOL and ZF on the Linux/x86
    2.39  platform.  The system may be easily built from scratch as well, taking
    2.40 -the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    2.41 -distributed with Isabelle for more information.
    2.42 +the traditional tar.gz source distribution.  See file <tt>INSTALL</tt>
    2.43 +as distributed with Isabelle for more information.
    2.44  
    2.45  Further background information may be found in the <em>Isabelle System
    2.46  Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    2.47  
    2.48  
    2.49 -<h2>User interfaces</h2>
    2.50 -
    2.51 -The distribution includes only a very primitive interface based on
    2.52 -ordinary terminal sessions. Advanced interfaces are available from
    2.53 -other sources:
    2.54 +<h2>User interface</h2>
    2.55  
    2.56 -<ul>
    2.57 -
    2.58 -<li>
    2.59 -<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    2.60 -David Aspinall and others is a generic Emacs interface for proof
    2.61 -assistants, including Isabelle (both for the classic and Isar
    2.62 +The canonical Isabelle user interface is <a
    2.63 +href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    2.64 +David Aspinall and others.  It is a generic (X)Emacs interface for
    2.65 +proof assistants, including Isabelle (both for the classic and Isar
    2.66  version).  Proof General is suitable for use by pacifists and Emacs
    2.67  militants alike. Its most prominent feature is script management,
    2.68  providing a metaphor of <em>live proof script editing</em>.  Proof
    2.69  General has recently gained a rather large following of both beginning
    2.70  and expert users of Isabelle.
    2.71  
    2.72 -<li>
    2.73 -<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    2.74 -David Aspinall is an older and simpler Emacs interface for Isabelle.
    2.75 -It runs under recent versions of XEmacs.
    2.76 +<p>
    2.77  
    2.78 -</ul>
    2.79 +Proof~General may be used together with the Emacs
    2.80 +<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
    2.81 +X-Symbol package</a>, which provides a nice way to get proper
    2.82 +mathematical symbols displayed on screen.
    2.83  
    2.84  
    2.85  <h2>Other sources of information</h2>
    2.86 @@ -145,9 +139,9 @@
    2.87  <p>
    2.88  
    2.89  <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
    2.90 -Institut fuer Informatik<br>
    2.91 -T. U. Muenchen<br>
    2.92 -D-80290 Muenchen<br>
    2.93 +Institut für Informatik<br>
    2.94 +T. U. München<br>
    2.95 +D-80290 München<br>
    2.96  Germany<br>
    2.97  <br>
    2.98  E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>