misc tuning for Isabelle2009;
authorwenzelm
Wed Apr 15 20:03:08 2009 +0200 (2009-04-15 ago)
changeset 3089816912b4e6625
parent 30897 44cba7df4003
child 30899 d394a17d4fdb
child 30933 0d126d4a3b0f
misc tuning for Isabelle2009;
INSTALL
README
     1.1 --- a/INSTALL	Wed Apr 15 19:52:45 2009 +0200
     1.2 +++ b/INSTALL	Wed Apr 15 20:03:08 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  ----------------------
     1.5  
     1.6  The Isabelle distribution includes both complete sources and
     1.7 -precompiled binary packages for common Unix platforms.
     1.8 +precompiled binary packages for common Unix-like platforms.
     1.9  
    1.10  
    1.11  Quick installation
     2.1 --- a/README	Wed Apr 15 19:52:45 2009 +0200
     2.2 +++ b/README	Wed Apr 15 20:03:08 2009 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4       * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
     2.5       * The GNU bash shell (version 3.x or 2.x).
     2.6       * Perl (version 5.x).
     2.7 -     * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
     2.8 +     * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x)
     2.9         -- for the Proof General interface.
    2.10       * A complete LaTeX installation -- for document preparation.
    2.11  
    2.12 @@ -22,9 +22,8 @@
    2.13  
    2.14     Binary packages are available for Isabelle/HOL and ZF for several
    2.15     platforms from the Isabelle web page. The system may be easily
    2.16 -   built from scratch as well, taking the traditional tar.gz source
    2.17 -   distribution. See file INSTALL as distributed with Isabelle for
    2.18 -   more information.
    2.19 +   built from scratch, using the tar.gz source distribution. See file
    2.20 +   INSTALL as distributed with Isabelle for more information.
    2.21  
    2.22     Further background information may be found in the Isabelle System
    2.23     Manual, distributed with the sources (directory doc).
    2.24 @@ -36,8 +35,8 @@
    2.25     including Isabelle. Proof General is suitable for use by pacifists
    2.26     and Emacs militants alike. Its most prominent feature is script
    2.27     management, providing a metaphor of live proof script editing.
    2.28 -   Proof General also provides some support for proper mathematical
    2.29 -   symbols displayed on screen.
    2.30 +   Proof General also provides some support for mathematical symbols
    2.31 +   displayed on screen.
    2.32  
    2.33  Other sources of information
    2.34