README
changeset 37159 07f3f5a03e98
parent 36858 8eac822dec6c
child 37368 1c816f2abb0e
     1.1 --- a/README	Thu May 27 21:37:42 2010 +0200
     1.2 +++ b/README	Fri May 28 11:23:34 2010 +0200
     1.3 @@ -9,8 +9,9 @@
     1.4  
     1.5  System requirements
     1.6  
     1.7 -   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
     1.8 -   following additional software:
     1.9 +   Isabelle requires a regular Unix-style platform (e.g. Linux,
    1.10 +   Windows with Cygwin, Mac OS) and depends on the following main
    1.11 +   add-on tools:
    1.12  
    1.13       * The Poly/ML compiler and runtime system (version 5.x).
    1.14       * The GNU bash shell (version 3.x or 2.x).
    1.15 @@ -20,7 +21,7 @@
    1.16  
    1.17  Installation
    1.18  
    1.19 -   Binary packages are available for Isabelle/HOL and ZF for several
    1.20 +   Binary packages are available for Isabelle/HOL etc. for several
    1.21     platforms from the Isabelle web page. The system may be also built
    1.22     from scratch, using the tar.gz source distribution. See file
    1.23     INSTALL as distributed with Isabelle for more information.
    1.24 @@ -32,9 +33,8 @@
    1.25  
    1.26     The classic Isabelle user interface is Proof General by David
    1.27     Aspinall and others. It is a generic Emacs interface for proof
    1.28 -   assistants, including Isabelle. Proof General is suitable for use
    1.29 -   by pacifists and Emacs militants alike. Its most prominent feature
    1.30 -   is script management, providing a metaphor of live proof script
    1.31 +   assistants, including Isabelle.  Its most prominent feature is
    1.32 +   script management, providing a metaphor of stepwise proof script
    1.33     editing.  Proof General also provides some support for mathematical
    1.34     symbols displayed on screen.
    1.35