# HG changeset patch
# User wenzelm
# Date 1195563313 -3600
# Node ID 880419e63924bb2594303b7372185c9d23ba5b2e
# Parent  c1be3072ea8f19a75cfc123c837bed1ae600f127
updated Proof General advertisement;
tuned line breaks;

diff -r c1be3072ea8f -r 880419e63924 README
--- a/README	Tue Nov 20 11:42:15 2007 +0100
+++ b/README	Tue Nov 20 13:55:13 2007 +0100
@@ -13,16 +13,16 @@
      * The GNU bash shell (version 3.x, 2.x).
      * Perl (version 5.x).
      * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22)
-       -- for the ProofGeneral interface.
+       -- for the Proof General interface.
      * A complete LaTeX installation -- for document preparation.
 
 Installation
 
    Binary packages are available for Isabelle/HOL and ZF for several
-   platforms from the Isabelle web page. The system may be easily built
-   from scratch as well, taking the traditional tar.gz source
-   distribution. See file INSTALL as distributed with Isabelle for more
-   information.
+   platforms from the Isabelle web page. The system may be easily
+   built from scratch as well, taking the traditional tar.gz source
+   distribution. See file INSTALL as distributed with Isabelle for
+   more information.
 
    Further background information may be found in the Isabelle System
    Manual, distributed with the sources (directory doc).
@@ -31,16 +31,14 @@
 
    The canonical Isabelle user interface is Proof General by David
    Aspinall and others. It is a generic (X)Emacs interface for proof
-   assistants, including Isabelle (both for the classic and Isar
-   version). Proof General is suitable for use by pacifists and Emacs
-   militants alike. Its most prominent feature is script management,
-   providing a metaphor of live proof script editing. Proof General has
-   recently gained a rather large following of both beginning and expert
-   users of Isabelle.
+   assistants, including Isabelle. Proof General is suitable for use
+   by pacifists and Emacs militants alike. Its most prominent feature
+   is script management, providing a metaphor of live proof script
+   editing.
 
    Proof General is distributed together with the XEmacs X-Symbol
-   package, which provides a nice way to get proper mathematical symbols
-   displayed on screen.
+   package, which provides a reasonable way to get proper mathematical
+   symbols displayed on screen.
 
 Other sources of information
 
@@ -53,8 +51,9 @@
   Mailing list
 
    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
-   forum for Isabelle users to discuss problems and exchange information.
-   To join, send a message to isabelle-users-request@cl.cam.ac.uk.
+   forum for Isabelle users to discuss problems and exchange
+   information.  To join, send a message to
+   isabelle-users-request@cl.cam.ac.uk.
 
   Personal mail
 
@@ -85,4 +84,3 @@
    helpful, we can accept no responsibility for the deficiencies of
    Isabelle and their consequences.
      _________________________________________________________________
-