From cb5622d4bfba6b6ab896eec698db80e19432f53e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 16 Jul 2002 17:15:32 +0000
Subject: Edit for brevity

---
 html/main.html | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

(limited to 'html')

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>
 
-- 
cgit v1.2.3