README.html
changeset 6077 60d97d521453
parent 5708 fb09ab6a447f
child 6125 59507030d953
     1.1 --- a/README.html	Mon Jan 11 10:22:04 1999 +0100
     1.2 +++ b/README.html	Mon Jan 11 12:50:29 1999 +0100
     1.3 @@ -14,32 +14,34 @@
     1.4  <h2>Version information</h2>
     1.5  
     1.6  This is the internal repository version of Isabelle.  Starting with
     1.7 -Isabelle98, the current line of Isabelle introduces many new features,
     1.8 -but also some incompatibilities with Isabelle94-XX.  See the
     1.9 -<tt>NEWS</tt> file in the distribution for more details.
    1.10 +Isabelle98, the current line of Isabelle development introduces many
    1.11 +new features, but also some incompatibilities with Isabelle94-XX.  See
    1.12 +the <tt>NEWS</tt> file in the distribution for more details.
    1.13  
    1.14  
    1.15  <h2>System requirements</h2>
    1.16  
    1.17  Isabelle requires a real Unix box with sufficient resources. Fun
    1.18 -starts at about 32MB of main memory (somewhat depending on your ML
    1.19 -system), with several tens of MB disk space and a relatively fast CPU.
    1.20 +starts at about 32-64 MB of main memory (somewhat depending on your ML
    1.21 +system), with several tens of MB disk space and a decent CPU.
    1.22 +Speaking by today's hardware standards, even a rather low-end Linux
    1.23 +box should make a nice platform for Isabelle.
    1.24  
    1.25  <p>
    1.26  
    1.27 -Furthermore, it needs the following software, which is not part of the
    1.28 -distribution:
    1.29 +Furthermore, Isabelle needs the following software, which is not part
    1.30 +of the distribution:
    1.31  <ul>
    1.32  <li> A full Standard ML Compiler (e.g. SML of New Jersey).
    1.33  <li> The GNU bash shell (version 1.x or 2.x).
    1.34  <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    1.35 -is *not* sufficient).
    1.36 +is <em>not</em> sufficient).
    1.37  </ul>
    1.38  
    1.39  <p>
    1.40  
    1.41  The following ML system and platform combinations are known to work
    1.42 -quite well:
    1.43 +very well:
    1.44  <ul>
    1.45  <li> SML/NJ 110.x on any Unix platform (e.g. Suns, Linux).
    1.46  <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    1.47 @@ -52,15 +54,18 @@
    1.48  <a
    1.49  href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
    1.50  needs lots of store and disk space, but it is free.  The current
    1.51 -official release is 110.  We also still support the old 0.93 release.
    1.52 +official release is 110 (there is an <a
    1.53 +href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
    1.54 +archive</a> available for Linux/x86).  We still support the old 0.93
    1.55 +release, but do not recommend to use it.
    1.56  
    1.57  <p>
    1.58  
    1.59  <a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a
    1.60 -commercial ML programming environment.  Isabelle on MLWorks 2.0 works well.
    1.61 -It is about 20% faster than on SML/NJ while using slightly less memory and
    1.62 -disk space.  A few minor features (e.g. top-level pretty printing) are not yet
    1.63 -supported, though.
    1.64 +commercial ML programming environment.  Isabelle on MLWorks 2.0 works
    1.65 +well.  It is about 20% faster than on SML/NJ while using slightly less
    1.66 +memory and disk space.  A few minor features (e.g. top-level pretty
    1.67 +printing) are not yet supported, though.
    1.68  
    1.69  <p>
    1.70  
    1.71 @@ -82,13 +87,24 @@
    1.72  <h2>Interfaces</h2>
    1.73  
    1.74  The distribution includes only a very primitive interface based on
    1.75 -ordinary terminal sessions.<p>
    1.76 +ordinary terminal sessions.
    1.77 +
    1.78 +<p>
    1.79  
    1.80  <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    1.81  David Aspinall is a more elaborate interface for Isabelle.  It runs
    1.82  under recent versions of XEmacs and is useful to both novices and
    1.83  experts.
    1.84  
    1.85 +<p>
    1.86 +
    1.87 +<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
    1.88 +a generic Emacs interface for proof assistants, including Isabelle (as
    1.89 +of version 2.0).  Proof General is suitable for use by pacifists and
    1.90 +Emacs militants alike. Its most prominent feature is script
    1.91 +management, providing a metaphor of <em>live proof script
    1.92 +editing</em>.
    1.93 +
    1.94  
    1.95  <h2>Other sources of information</h2>
    1.96