Edit for brevity

1 files changed, 9 insertions, 11 deletions

diff --git a/html/main.html b/html/main.html
index d6672b96..a4a37b54 100644
--- a/html/main.html
+++ b/html/main.html
@@ -1,21 +1,19 @@
 <h2>What is Proof General?</h2>
 <p>
 <b>Proof General</b> is a generic interface for proof assistants, 
-currently based on Emacs.
-It has been developed at the
+currently based on the customizable text editor <i>Emacs</i>.
+It works with either
+<a href="http://www.xemacs.org/">XEmacs</a> or
+<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
+Proof General has been developed at the
 <a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>
 in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>.
-Proof General 
-works best under 
-<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with 
-<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
-You need a recent version in either case.
 </p>
 <p>
-To read more about what Proof General
-is and what it provides, 
+To read more about Proof General
+and what it provides, 
 <a href="features">check the features list</a>.
-To see what Proof General looks like in use, have a look at these
+To see Proof General in use, have a look at these
 <a href="screenshot">screenshots</a>.
 To download Proof General, visit the
 <a href="download">download page</a>.
@@ -126,7 +124,7 @@ seeking volunteers to support and improve each of these
 Proof General is ready to be customized to new proof assistants.
 It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
 "very easy"); ?> to get basic support working.
-Full <a href="ProofGeneral/doc/PG-adapting.pdf">documentation on 
+Full <a href="doc">documentation on 
 configuration</a> is provided.
 </p>