Renamed files

2 files changed, 223 insertions, 0 deletions

diff --git a/html/download.html b/html/download.html
new file mode 100644
index 00000000..03948ac0
--- /dev/null
+++ b/html/download.html
@@ -0,0 +1,214 @@
+<h2>Please register</h2>
+<p>
+Before downloading Proof General, <i>please</i>
+<a href="register.html">register</a>.
+It's free, it only takes a moment.
+If you have already registered you do not need to do so again.
+</p>
+<p>
+The statistics collected from registrations will be used to help a
+case for support for Proof General, and nothing else.  It is likely
+that development of Proof General will <i>finish very soon</i> unless
+we can find new resources.  As a courtesy, we do not make registration
+compulsory and I can tell from the server logs that the majority of  
+people downloading do not register.  But if you don't register
+now, please consider returning to register later if you find Proof
+General interesting or useful.  If you don't want to fill the form,
+please <a href="mailto:proofgen@dcs.ed.ac.uk">send an email</a>
+directly.
+</p>
+
+<p>
+You may like to join the
+Proof General
+<a href="mailinglist.html">mailing list</a>.
+Developers and beta-testers may like to download
+a <a href="develdownload.html">development release</a>
+of Proof General.
+If you use an old version of a proof assistant,
+you may need to download one of the 
+<a href="oldrel.html">previous releases</a>.
+</p>
+<p>
+Please check the 
+<?php fileshow("ProofGeneral/COPYING","license conditions "); ?>
+for using Proof General.
+</p>
+
+<h2><a name="prereq">
+    What you need to run Proof General
+    </a>
+</h2>
+<p>
+To run Proof General, you <strong>must</strong> have:
+</p>
+<ul>
+<li>
+Version 21.1 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.5 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 Windows 95/98/NT.
+</li>
+<li>
+One or more of the supported proof assistants.  Or write your own
+support for a new assistant.  
+<br>
+See the 
+<?php link_root("main","front page") ?> for links to supported
+assistants.
+</li>
+</ul>
+<p>
+
+There are also some <strong>optional</strong> components for using
+Proof General:
+<ul>
+<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>It's very easy to install.  See <a href="#xsyminstall">here</a> 
+for installation notes.
+<br>X-Symbol presently only works with XEmacs on systems running X.  
+</li>
+<!-- <li> -->
+<!-- For FSF Emacs, a version of <tt>func-menu.el</tt> to get  -->
+<!-- <?php link_root("features#funcmenu","function menus") ?>. -->
+<!-- <br>Unfortunately I can't find a version of this that -->
+<!-- works with current FSF Emacs releases. I'd be grateful  -->
+<!-- for a pointer to one.   -->
+<!-- <br> -->
+<!-- (The package  -->
+<!-- <tt>imenu.el</tt> may be a suitable replacement, -->
+<!-- and it ships with both Emacsen.  Perhaps   -->
+<!-- somebody could contribute patches to use that  -->
+<!-- instead of <tt>func-menu</tt>). -->
+</ul>
+<p>
+All components mentioned above are distributed under the GPL license.
+</p>
+<br>
+<br>
+
+
+<h2><a name="stable">
+    Proof General Version 3.1, released 23rd March 2000
+    </a>
+</h2>
+
+<p>
+Proof General is available as an archive and an RPM package.
+</p>
+<ul>
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-3.1.tar.gz") ?>,
+      <br>
+      or the same thing in a zip file:
+      <?php download_link("ProofGeneral-3.1.zip") ?>,
+  </li>
+ <li> Linux RPM package:
+      <?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?>
+     <br>
+     You probably don't need the 
+      <?php download_link("ProofGeneral-3.1-1.src.rpm",
+	"source RPM") ?>.
+ </li>
+</ul>
+<p>
+Both the tarball and the RPM package include the generic elisp
+code, <br>
+code for LEGO, Coq, and Isabelle, installation instructions
+and documentation (in Info and HTML formats).
+</p>
+<p>
+Documentation is available in other formats
+here <?php link_root("doc","here") ?>.  
+If you want to format the documentation yourself,
+you may like to download the
+<?php download_link("ProofGeneralPortrait.eps.gz", 
+"front page image") ?>.
+</p>
+
+<p>
+This version of Proof General has been tested
+with XEmacs 21.1 and FSF Emacs 20.4.
+It supports Coq version 6.3, LEGO version 1.3.1 and
+Isabelle99.
+</p>
+<p>
+Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file
+for a summary of changes since version 3.0.
+</p>
+<p>
+Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file
+(also 
+<?php fileshow("ProofGeneral/lego/BUGS","lego/BUGS, "); ?>
+<?php fileshow("ProofGeneral/coq/BUGS","coq/BUGS, "); ?>
+<?php fileshow("ProofGeneral/isa/BUGS","isa/BUGS, "); ?>
+<?php fileshow("ProofGeneral/isar/BUGS","isar/BUGS," ); ?>)
+<!-- <?php fileshow("ProofGeneral/hol98/BUGS","hol98/BUGS"); ?>) -->
+before reporting problems.  If you find a problem not already mentioned, 
+please 
+<?php hlink("feedback.html","send us a note","Feedback form")?>.
+</p>
+<br>
+<br>
+
+<h3><a name="install">Easy installation</a></h3> 
+<p>
+To use Proof General, simply unpack the sources with 
+</p>
+ <blockquote>
+   <tt>tar xpzf ProofGeneral-3.1.tar.gz</tt>
+ </blockquote>
+<p>
+(use <tt>gunzip</tt> first in place of <tt>z</tt> if you don't have
+GNU tar),<br> and then add this one line to your .emacs file:
+</p>
+ <blockquote>
+  <tt> (load-file "<var>directory</var>/generic/proof-site.el")</tt>
+ </blockquote>
+<p>
+Where <var>directory</var> is the directory in which you unpacked
+the sources.  
+<br>
+If you use the RPM package, <var>directory</var> is
+<tt>/usr/share/emacs/ProofGeneral</tt>
+</p>
+<p>
+If you're using Windows, then download the zip file.
+<br> 
+Use a zip file utility to unpack it somewhere, for example
+<tt>c:\\ProofGeneral</tt>
+</p>
+<p>
+Further customization is possible via the Customize menus in
+Emacs.  
+<br>
+See the <?php fileshow("ProofGeneral-3.1/INSTALL","INSTALL")?> 
+file in the distribution for more details.
+</p>
+
+<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> 
+
+<p>
+Contrary to what you may expect from the documentation of
+X-Symbol, it's very easy to install and configures itself
+automatically.
+</p>
+<p>
+Simply download the binary package file, and do something
+like this to install in your home directory:
+</p>
+<blockquote><tt>
+ mkdir -p ~/.xemacs<br>
+ cd ~/.xemacs<br>
+ tar xpzf ../x-symbol-pkg.tar.gz<br>
+</tt></blockquote>
diff --git a/html/index.html b/html/index.html
new file mode 100644
index 00000000..f0cbe7a1
--- /dev/null
+++ b/html/index.html
@@ -0,0 +1,9 @@
+<?php require('functions.php3'); ?>
+<html>
+<?php  include('head.html'); ?>
+<?php
+    include('header.html');
+    include($WANTED . '.html');
+    footer();
+?>
+