README
changeset 25447 880419e63924
parent 25415 02884a4e1ac6
child 27006 6ca0c942a25c
     1.1 --- a/README	Tue Nov 20 11:42:15 2007 +0100
     1.2 +++ b/README	Tue Nov 20 13:55:13 2007 +0100
     1.3 @@ -13,16 +13,16 @@
     1.4       * The GNU bash shell (version 3.x, 2.x).
     1.5       * Perl (version 5.x).
     1.6       * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22)
     1.7 -       -- for the ProofGeneral interface.
     1.8 +       -- for the Proof General interface.
     1.9       * A complete LaTeX installation -- for document preparation.
    1.10  
    1.11  Installation
    1.12  
    1.13     Binary packages are available for Isabelle/HOL and ZF for several
    1.14 -   platforms from the Isabelle web page. The system may be easily built
    1.15 -   from scratch as well, taking the traditional tar.gz source
    1.16 -   distribution. See file INSTALL as distributed with Isabelle for more
    1.17 -   information.
    1.18 +   platforms from the Isabelle web page. The system may be easily
    1.19 +   built from scratch as well, taking the traditional tar.gz source
    1.20 +   distribution. See file INSTALL as distributed with Isabelle for
    1.21 +   more information.
    1.22  
    1.23     Further background information may be found in the Isabelle System
    1.24     Manual, distributed with the sources (directory doc).
    1.25 @@ -31,16 +31,14 @@
    1.26  
    1.27     The canonical Isabelle user interface is Proof General by David
    1.28     Aspinall and others. It is a generic (X)Emacs interface for proof
    1.29 -   assistants, including Isabelle (both for the classic and Isar
    1.30 -   version). Proof General is suitable for use by pacifists and Emacs
    1.31 -   militants alike. Its most prominent feature is script management,
    1.32 -   providing a metaphor of live proof script editing. Proof General has
    1.33 -   recently gained a rather large following of both beginning and expert
    1.34 -   users of Isabelle.
    1.35 +   assistants, including Isabelle. Proof General is suitable for use
    1.36 +   by pacifists and Emacs militants alike. Its most prominent feature
    1.37 +   is script management, providing a metaphor of live proof script
    1.38 +   editing.
    1.39  
    1.40     Proof General is distributed together with the XEmacs X-Symbol
    1.41 -   package, which provides a nice way to get proper mathematical symbols
    1.42 -   displayed on screen.
    1.43 +   package, which provides a reasonable way to get proper mathematical
    1.44 +   symbols displayed on screen.
    1.45  
    1.46  Other sources of information
    1.47  
    1.48 @@ -53,8 +51,9 @@
    1.49    Mailing list
    1.50  
    1.51     The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    1.52 -   forum for Isabelle users to discuss problems and exchange information.
    1.53 -   To join, send a message to isabelle-users-request@cl.cam.ac.uk.
    1.54 +   forum for Isabelle users to discuss problems and exchange
    1.55 +   information.  To join, send a message to
    1.56 +   isabelle-users-request@cl.cam.ac.uk.
    1.57  
    1.58    Personal mail
    1.59  
    1.60 @@ -85,4 +84,3 @@
    1.61     helpful, we can accept no responsibility for the deficiencies of
    1.62     Isabelle and their consequences.
    1.63       _________________________________________________________________
    1.64 -