diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/about.html (renamed from html/about.phtml) | 0 | ||||
| -rw-r--r-- | html/devel.html (renamed from html/devel.phtml) | 0 | ||||
| -rw-r--r-- | html/develdownload.html (renamed from html/develdownload.phtml) | 2 | ||||
| -rw-r--r-- | html/doc.html (renamed from html/doc.phtml) | 0 | ||||
| -rw-r--r-- | html/download.phtml | 214 | ||||
| -rw-r--r-- | html/features.html (renamed from html/features.phtml) | 0 | ||||
| -rw-r--r-- | html/feedback.html (renamed from html/feedback.phtml) | 0 | ||||
| -rw-r--r-- | html/fileshow.html (renamed from html/fileshow.phtml) | 0 | ||||
| -rw-r--r-- | html/footer.html (renamed from html/footer.phtml) | 0 | ||||
| -rw-r--r-- | html/gallery.html (renamed from html/gallery.phtml) | 0 | ||||
| -rw-r--r-- | html/head.html (renamed from html/head.phtml) | 0 | ||||
| -rw-r--r-- | html/header.html (renamed from html/header.phtml) | 0 | ||||
| -rw-r--r-- | html/hits.html (renamed from html/hits.phtml) | 0 | ||||
| -rw-r--r-- | html/htmlshow.html (renamed from html/htmlshow.phtml) | 0 | ||||
| -rw-r--r-- | html/index.phtml | 9 | ||||
| -rw-r--r-- | html/links.html (renamed from html/links.phtml) | 0 | ||||
| -rw-r--r-- | html/mailinglist.html (renamed from html/mailinglist.phtml) | 0 | ||||
| -rw-r--r-- | html/main.html (renamed from html/main.phtml) | 0 | ||||
| -rw-r--r-- | html/mission.html (renamed from html/mission.phtml) | 0 | ||||
| -rw-r--r-- | html/news.html (renamed from html/news.phtml) | 0 | ||||
| -rw-r--r-- | html/oldnews.html (renamed from html/oldnews.phtml) | 0 | ||||
| -rw-r--r-- | html/oldrel.html (renamed from html/oldrel.phtml) | 0 | ||||
| -rw-r--r-- | html/projects.html (renamed from html/projects.phtml) | 0 | ||||
| -rw-r--r-- | html/register.html (renamed from html/register.phtml) | 0 | ||||
| -rw-r--r-- | html/screenshot.html (renamed from html/screenshot.phtml) | 0 | ||||
| -rw-r--r-- | html/smallheader.html (renamed from html/smallheader.phtml) | 0 | ||||
| -rw-r--r-- | html/smallpage.html (renamed from html/smallpage.phtml) | 0 |
27 files changed, 2 insertions, 223 deletions
diff --git a/html/about.phtml b/html/about.html index 7641676d..7641676d 100644 --- a/html/about.phtml +++ b/html/about.html diff --git a/html/devel.phtml b/html/devel.html index aa418f08..aa418f08 100644 --- a/html/devel.phtml +++ b/html/devel.html diff --git a/html/develdownload.phtml b/html/develdownload.html index 499a0b15..bacdc0c9 100644 --- a/html/develdownload.phtml +++ b/html/develdownload.html @@ -45,10 +45,12 @@ or <!-- WARNING! Line below automatically edited by makefile. --> <h2><a name="prerel">Pre-release: ProofGeneral-3.2pre000928</a></h2> +<p> This version has been tested with XEmacs version 21.1.12 and (minimally) with FSF Emacs 20.7.1. We recommend the use of XEmacs; use under FSF Emacs can no longer be supported. +</p> <p> Check the <!-- WARNING! Line below automatically edited by makefile. --> diff --git a/html/doc.phtml b/html/doc.html index e8ae6b98..e8ae6b98 100644 --- a/html/doc.phtml +++ b/html/doc.html diff --git a/html/download.phtml b/html/download.phtml deleted file mode 100644 index 7ddf5585..00000000 --- a/html/download.phtml +++ /dev/null @@ -1,214 +0,0 @@ -<h2>Please register</h2> -<p> -Before downloading Proof General, <i>please</i> -<a href="register.phtml">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.phtml">mailing list</a>. -Developers and beta-testers may like to download -a <a href="develdownload.phtml">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.phtml">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.phtml","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/features.phtml b/html/features.html index 372ab17b..372ab17b 100644 --- a/html/features.phtml +++ b/html/features.html diff --git a/html/feedback.phtml b/html/feedback.html index 17dc974c..17dc974c 100644 --- a/html/feedback.phtml +++ b/html/feedback.html diff --git a/html/fileshow.phtml b/html/fileshow.html index a13857e7..a13857e7 100644 --- a/html/fileshow.phtml +++ b/html/fileshow.html diff --git a/html/footer.phtml b/html/footer.html index 9fd59285..9fd59285 100644 --- a/html/footer.phtml +++ b/html/footer.html diff --git a/html/gallery.phtml b/html/gallery.html index e433da8a..e433da8a 100644 --- a/html/gallery.phtml +++ b/html/gallery.html diff --git a/html/head.phtml b/html/head.html index c40263e7..c40263e7 100644 --- a/html/head.phtml +++ b/html/head.html diff --git a/html/header.phtml b/html/header.html index e5100744..e5100744 100644 --- a/html/header.phtml +++ b/html/header.html diff --git a/html/hits.phtml b/html/hits.html index 6d5c2be6..6d5c2be6 100644 --- a/html/hits.phtml +++ b/html/hits.html diff --git a/html/htmlshow.phtml b/html/htmlshow.html index d9cb8b46..d9cb8b46 100644 --- a/html/htmlshow.phtml +++ b/html/htmlshow.html diff --git a/html/index.phtml b/html/index.phtml deleted file mode 100644 index 979f1e04..00000000 --- a/html/index.phtml +++ /dev/null @@ -1,9 +0,0 @@ -<?php require('functions.php3'); ?> -<html> -<?php include('head.phtml'); ?> -<?php - include('header.phtml'); - include($WANTED . '.phtml'); - footer(); -?> - diff --git a/html/links.phtml b/html/links.html index 32ac9782..32ac9782 100644 --- a/html/links.phtml +++ b/html/links.html diff --git a/html/mailinglist.phtml b/html/mailinglist.html index b6336f45..b6336f45 100644 --- a/html/mailinglist.phtml +++ b/html/mailinglist.html diff --git a/html/main.phtml b/html/main.html index 7844d527..7844d527 100644 --- a/html/main.phtml +++ b/html/main.html diff --git a/html/mission.phtml b/html/mission.html index deec79dc..deec79dc 100644 --- a/html/mission.phtml +++ b/html/mission.html diff --git a/html/news.phtml b/html/news.html index f717ad77..f717ad77 100644 --- a/html/news.phtml +++ b/html/news.html diff --git a/html/oldnews.phtml b/html/oldnews.html index 4078fd73..4078fd73 100644 --- a/html/oldnews.phtml +++ b/html/oldnews.html diff --git a/html/oldrel.phtml b/html/oldrel.html index 9aa952ff..9aa952ff 100644 --- a/html/oldrel.phtml +++ b/html/oldrel.html diff --git a/html/projects.phtml b/html/projects.html index a8c180aa..a8c180aa 100644 --- a/html/projects.phtml +++ b/html/projects.html diff --git a/html/register.phtml b/html/register.html index 4390ef83..4390ef83 100644 --- a/html/register.phtml +++ b/html/register.html diff --git a/html/screenshot.phtml b/html/screenshot.html index b57c0d37..b57c0d37 100644 --- a/html/screenshot.phtml +++ b/html/screenshot.html diff --git a/html/smallheader.phtml b/html/smallheader.html index 8cf93a42..8cf93a42 100644 --- a/html/smallheader.phtml +++ b/html/smallheader.html diff --git a/html/smallpage.phtml b/html/smallpage.html index 64f538a3..64f538a3 100644 --- a/html/smallpage.phtml +++ b/html/smallpage.html |