Section on what you need for PG

1 files changed, 43 insertions, 0 deletions

diff --git a/html/download.phtml b/html/download.phtml
index c446cce6..1d168537 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -28,6 +28,49 @@ you may need to download one of the
 </p>
 <hr>
 
+<h2><a name="prereq">
+    What you need to run Proof General
+    </a>
+</h2>
+<p>
+To run Proof General, you should have:
+</p>
+<ul>
+<li>
+Version 20.4 or later of <a href="http://www.xemacs.org">XEmacs</a>
+(this UK 
+<a href="http://sunsite.doc.ic.ac.uk/Mirrors/ftp.xemacs.org/pub/xemacs/">
+ftp mirror</a> may help).
+<br>
+<b>or</b> version 20.2 or later of the much poorer 
+<a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
+<br>
+Both Emacsen are available for a variety of platforms, including
+Unix variants and NT.
+</li>
+<li>
+For displaying logical and mathematical symbols, the excellent
+<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
+package. 
+<br>X-Symbol presently only works with XEmacs.  
+Its use with Proof General is optional.
+</li>
+<li>
+For FSF Emacs, a version of <tt>func-menu.el</tt> to get 
+<?php link_root("features#funcmenu","function menus") ?>.
+<br>I haven't been able to find a recent version of this that
+works with FSF Emacs, I'd be grateful if anyone can send me
+a pointer or a hacked version which does. 
+Proof General works fine without this feature.
+</ul>
+<p>
+All these components are distributed under the 
+GPL license.
+</p>
+<br>
+<br>
+
+
 <h2><a name="stable">
     Proof General Version 2.1, released 24th August 1999
     </a>