1.1 --- a/README.html	Mon Sep 11 20:24:06 2000 +0200
     1.2 +++ b/README.html	Mon Sep 11 20:41:44 2000 +0200
     1.3 @@ -13,16 +13,16 @@
     1.4  <h2>Version information</h2>
     1.5  
     1.6  This is the internal repository version of Isabelle.  The current line
     1.7 -of development introduces many new features, while attempting to keep
     1.8 -incompatibilities over Isabelle98-X at a minimum.  See the
     1.9 -<tt>NEWS</tt> file in the distribution for more details.
    1.10 +of Isabelle99 development introduces many new concepts, while
    1.11 +attempting to keep incompatibilities over Isabelle98 at a minimum.
    1.12 +See 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 32-64 MB of free main memory (somewhat depending on
    1.19 -your ML system), with several tens of MB disk space and a decent CPU.
    1.20 +the ML system), with several tens of MB disk space and a decent CPU.
    1.21  Speaking by today's hardware standards, any moderate Linux box should
    1.22  give a very nice platform for Isabelle.
    1.23  
    1.24 @@ -42,7 +42,7 @@
    1.25  The following ML system and platform combinations are known to work
    1.26  very well:
    1.27  <ul>
    1.28 -<li> Poly/ML 3.x on Linux and Sparc/Solaris.
    1.29 +<li> Poly/ML 3.x on Linux/x86 and Solaris/Sparc.
    1.30  <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    1.31  </ul>
    1.32  
    1.33 @@ -68,39 +68,33 @@
    1.34  
    1.35  <h2>Installation</h2>
    1.36  
    1.37 -RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    1.38 +Binary packages are available for Isabelle/HOL and ZF on the Linux/x86
    1.39  platform.  The system may be easily built from scratch as well, taking
    1.40 -the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    1.41 -distributed with Isabelle for more information.
    1.42 +the traditional tar.gz source distribution.  See file <tt>INSTALL</tt>
    1.43 +as distributed with Isabelle for more information.
    1.44  
    1.45  Further background information may be found in the <em>Isabelle System
    1.46  Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    1.47  
    1.48  
    1.49 -<h2>User interfaces</h2>
    1.50 +<h2>User interface</h2>
    1.51  
    1.52 -The distribution includes only a very primitive interface based on
    1.53 -ordinary terminal sessions. Advanced interfaces are available from
    1.54 -other sources:
    1.55 -
    1.56 -<ul>
    1.57 -
    1.58 -<li>
    1.59 -<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    1.60 -David Aspinall and others is a generic Emacs interface for proof
    1.61 -assistants, including Isabelle (both for the classic and Isar
    1.62 +The canonical Isabelle user interface is <a
    1.63 +href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    1.64 +David Aspinall and others.  It is a generic (X)Emacs interface for
    1.65 +proof assistants, including Isabelle (both for the classic and Isar
    1.66  version).  Proof General is suitable for use by pacifists and Emacs
    1.67  militants alike. Its most prominent feature is script management,
    1.68  providing a metaphor of <em>live proof script editing</em>.  Proof
    1.69  General has recently gained a rather large following of both beginning
    1.70  and expert users of Isabelle.
    1.71  
    1.72 -<li>
    1.73 -<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    1.74 -David Aspinall is an older and simpler Emacs interface for Isabelle.
    1.75 -It runs under recent versions of XEmacs.
    1.76 +<p>
    1.77  
    1.78 -</ul>
    1.79 +Proof~General may be used together with the Emacs
    1.80 +<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
    1.81 +X-Symbol package</a>, which provides a nice way to get proper
    1.82 +mathematical symbols displayed on screen.
    1.83  
    1.84  
    1.85  <h2>Other sources of information</h2>
    1.86 @@ -145,9 +139,9 @@
    1.87  <p>
    1.88  
    1.89  <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
    1.90 -Institut fuer Informatik<br>
    1.91 -T. U. Muenchen<br>
    1.92 -D-80290 Muenchen<br>
    1.93 +Institut für Informatik<br>
    1.94 +T. U. München<br>
    1.95 +D-80290 München<br>
    1.96  Germany<br>
    1.97  <br>
    1.98  E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>