1.1 --- a/README	Thu Apr 02 14:09:41 2009 +0200
     1.2 +++ b/README	Thu Apr 02 14:30:16 2009 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5     Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
     1.6     following additional software:
     1.7 -     * A full Standard ML Compiler (works best with Poly/ML 5.x).
     1.8 +     * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
     1.9       * The GNU bash shell (version 3.x or 2.x).
    1.10       * Perl (version 5.x).
    1.11       * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
    1.12 @@ -31,15 +31,12 @@
    1.13  
    1.14  User interface
    1.15  
    1.16 -   The canonical Isabelle user interface is Proof General by David
    1.17 -   Aspinall and others. It is a generic (X)Emacs interface for proof
    1.18 -   assistants, including Isabelle. Proof General is suitable for use
    1.19 -   by pacifists and Emacs militants alike. Its most prominent feature
    1.20 -   is script management, providing a metaphor of live proof script
    1.21 -   editing.
    1.22 -
    1.23 -   Proof General is distributed together with the XEmacs X-Symbol
    1.24 -   package, which provides a reasonable way to get proper mathematical
    1.25 +   The main Isabelle user interface is Proof General by David Aspinall
    1.26 +   and others. It is a generic Emacs interface for proof assistants,
    1.27 +   including Isabelle. Proof General is suitable for use by pacifists
    1.28 +   and Emacs militants alike. Its most prominent feature is script
    1.29 +   management, providing a metaphor of live proof script editing.
    1.30 +   Proof General also provides some support for proper mathematical
    1.31     symbols displayed on screen.
    1.32  
    1.33  Other sources of information