Deleted file

127 files changed, 0 insertions, 5553 deletions

diff --git a/html/.cvsignore b/html/.cvsignore
deleted file mode 100644
index d6e10bc1..00000000
--- a/html/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-ProofGeneral
diff --git a/html/.htaccess b/html/.htaccess
deleted file mode 100644
index 81c0ea37..00000000
--- a/html/.htaccess
+++ /dev/null
@@ -1,5 +0,0 @@
-RemoveHandler .html
-AddType application/x-httpd-php .html
-# support old address of zermelo.dcs.ed.ac.uk/~proofgen
-Redirect /~proofgen http://proofgeneral.inf.ed.ac.uk/
-Redirect /home/proofgen http://proofgeneral.inf.ed.ac.uk/
diff --git a/html/FAQ b/html/FAQ
deleted file mode 100644
index 4422a8f0..00000000
--- a/html/FAQ
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php require('functions.php3');
-      require('elispmarkup.php3');
-      fileshowmarkup("ProofGeneral/FAQ",
-		     "Frequently Asked Questions about using Proof General");
-?>
diff --git a/html/Kit/.htaccess b/html/Kit/.htaccess
deleted file mode 100644
index c22265e7..00000000
--- a/html/Kit/.htaccess
+++ /dev/null
@@ -1 +0,0 @@
-# Options -Indexes
diff --git a/html/Kit/Makefile b/html/Kit/Makefile
deleted file mode 100644
index 3a4e7591..00000000
--- a/html/Kit/Makefile
+++ /dev/null
@@ -1,16 +0,0 @@
-#
-# Update exported Kit files from PG Kit repository.
-# [interim]
-#
-
-.PHONY: update
-
-CVSROOT=:pserver:da@cvs.inf.ed.ac.uk:/disk/cvs/proofgen
-
-# checkout in temp dir because otherwise CVS complains of working dir checkout
-update:	
-	mkdir kittmp
-	cvs -d ${CVSROOT} export -kv -D today -d kittmp kitwebfiles
-	(cd kittmp; tar -c . | (cd ..; tar -xp))
-	rm -rf kittmp
-	cvs commit -m"Updated from Kit repo"
diff --git a/html/Kit/docs/commentary.pdf b/html/Kit/docs/commentary.pdf
deleted file mode 100644
index 1fe871f5..00000000
--- a/html/Kit/docs/commentary.pdf
+++ /dev/null
diff --git a/html/Kit/docs/uitp03.pdf b/html/Kit/docs/uitp03.pdf
deleted file mode 100644
index ebcae29c..00000000
--- a/html/Kit/docs/uitp03.pdf
+++ /dev/null
diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd
deleted file mode 100644
index 8210331d..00000000
--- a/html/Kit/dtd/pgip.dtd
+++ /dev/null
@@ -1,593 +0,0 @@
-<?xml encoding="UTF-8"?>
-
-<!--
-
-RELAX NG Schema for PGIP, the Proof General Interface Protocol                   
-
-Authors:  David Aspinall, LFCS, University of Edinburgh       
-          Christoph Lueth, University of Bremen       
-
-Version: pgip.dtd,v 1.27 2003/09/23 23:17:18 da Exp    
-
-Status:  Experimental.                                           
-For additional commentary, see the Proof General Kit white paper,
-available from http://www.proofgeneral.org/kit
-
-Advertised version: 1.0
-
--->
-
-<!ENTITY % pgml SYSTEM "pgml.dtd">
-%pgml;
-
-<!-- include PGML grammar -->
-
-<!-- ========== PGIP MESSAGES ========== -->
-
-<!-- complete construction of the currently open theory -->
-
-<!ENTITY % improperfilecmd "aborttheory|retracttheory|openfile|closefile
-                            |abortfile|loadfile|changecwd">
-
-<!ENTITY % properfilecmd "opentheory|closetheory">
-
-<!-- a "literate" comment: text processed by prover, but no sidefx -->
-
-<!ENTITY % improperproofcmd "undostep|abortgoal|forget|restoregoal">
-
-<!ENTITY % properproofcmd "opengoal|proofstep|closegoal|postponegoal
-                           |giveupgoal|comment|litcomment">
-
-<!-- change prover's working directory (or load path) for files -->
-
-<!ENTITY % fileinfomsg "informfileloaded|informfileretracted">
-
-<!-- ========== GENERAL PROVER OUTPUT/RESPONSES ========== -->
-
-<!ENTITY % proveroutput "ready|cleardisplay|normalresponse|errorresponse
-                         |scriptinsert|metainforesponse|parseresult
-                         |unparseresult">
-
-<!--  ========== INTERFACE CONFIGURATION ========== -->
-
-<!ENTITY % kitconfig "usespgip|usespgml|pgmlconfig|proverinfo|hasprefs
-                      |prefval|guiconfig|setids|addids|delids|idvalue
-                      |menuadd|menudel">
-
-<!-- ========== THEORY/FILE HANDLING COMMANDS ========== -->
-
-<!ENTITY % filecmd "%properfilecmd;|%improperfilecmd;">
-
-<!-- ========= PROOF CONTEXT/ETC COMMANDS =========== -->
-
-<!ENTITY % proofctxt "askids|showid|setid|parsescript|unparsecmds
-                      |showproofstate|showctxt|searchtheorems
-                      |setlinewidth|viewdoc">
-
-<!-- data values -->
-
-<!-- ========== PROOF CONTROL COMMANDS ========== -->
-
-<!ENTITY % proofcmd "%properproofcmd;|%improperproofcmd;">
-
-<!-- text is arg to "viewdoc" -->
-
-<!-- ========== PROVER CONTROL ========== -->
-
-<!ENTITY % provercontrol "proverinit|proverexit|startquiet|stopquiet
-                          |pgmlsymbolson|pgmlsymbolsoff">
-
-<!-- information messages concerning  -->
-
-<!--  ========== PROVER CONFIGURATION ========== -->
-
-<!ENTITY % proverconfig "askpgip|askpgml|askconfig|askprefs|setpref
-                         |getpref">
-
-<!-- issue a file command -->
-
-<!ENTITY % kitmsg "%kitconfig;|%proveroutput;|%fileinfomsg;">
-
-<!-- for a message sent TO proof general -->
-
-<!ENTITY % provermsg "%proverconfig;|%provercontrol;|%proofcmd;
-                      |%proofctxt;|%filecmd;">
-
-<!--
-pgips is the type of a log between
-two components.
--->
-
-<!ELEMENT pgip (%provermsg;|%kitmsg;)>
-
-<!-- or an interface message -->
-
-<!ELEMENT pgips (pgip)+>
-
-<!-- sequence number of this message -->
-
-<!ENTITY % pgip_class "pa|pg">
-
-<!ATTLIST pgip
-  origin CDATA #IMPLIED
-  id CDATA #REQUIRED
-  class (%pgip_class;) #REQUIRED
-  refseq CDATA #IMPLIED
-  refid CDATA #IMPLIED
-  seq CDATA #REQUIRED>
-
-<!-- please tell me this preference value -->
-
-<!ENTITY % name_attr "
-  name CDATA #REQUIRED">
-
-<!-- identifiers must be XML tokens -->
-
-<!ENTITY % prefcat_attr "
-  prefcategory CDATA #REQUIRED">
-
-<!--
-e.g. "expert", "internal", etc.
-could be used for tabs in dialog
--->
-
-<!ELEMENT askpgip EMPTY>
-
-<!ELEMENT askpgml EMPTY>
-
-<!ELEMENT askconfig EMPTY>
-
-<!ELEMENT askprefs EMPTY>
-<!ATTLIST askprefs
-  prefcategory CDATA #IMPLIED>
-
-<!ELEMENT setpref (#PCDATA)>
-<!ATTLIST setpref
-  %name_attr;
-  prefcategory CDATA #IMPLIED>
-
-<!ELEMENT getpref EMPTY>
-<!ATTLIST getpref
-  %name_attr;
-  prefcategory CDATA #IMPLIED>
-
-<!-- remove a menu entry -->
-
-<!-- version reporting -->
-
-<!ENTITY % version_attr "
-  version CDATA #REQUIRED">
-
-<!ELEMENT usespgml EMPTY>
-<!ATTLIST usespgml
-  %version_attr;>
-
-<!ELEMENT usespgip EMPTY>
-<!ATTLIST usespgip
-  %version_attr;>
-
-<!-- PGML configuration -->
-
-<!ELEMENT pgmlconfig (%pgmlconfigure;)+>
-
-<!--
-Types for config settings: corresponding data values should conform
-to representation for corresponding XML Schema 1.0 Datatypes.
-(This representation is verbose but helps for error checking later)
--->
-
-<!ENTITY % pgiptype "pgipbool|pgipint|pgipstring|pgipchoice">
-
-<!ELEMENT pgipbool EMPTY>
-
-<!ELEMENT pgipint EMPTY>
-<!ATTLIST pgipint
-  min CDATA #IMPLIED
-  max CDATA #IMPLIED>
-
-<!ENTITY % min_attr "
-  min CDATA #REQUIRED">
-
-<!ENTITY % max_attr "
-  max CDATA #REQUIRED">
-
-<!ELEMENT pgipstring EMPTY>
-
-<!ELEMENT pgipchoice (pgipchoiceitem)+>
-
-<!ELEMENT pgipchoiceitem (#PCDATA)>
-
-<!ELEMENT icon (#PCDATA)>
-
-<!-- image data for an icon -->
-
-<!-- preferences -->
-
-<!ENTITY % default_attr "
-  default CDATA #REQUIRED">
-
-<!ENTITY % descr_attr "
-  descr CDATA #REQUIRED">
-
-<!--
-icons for preference recommended size: 32x32 
-top level preferences: may be used in dialog for preference setting
-object preferences: may be used as an "emblem" to decorate 
-object icon (boolean preferences with default false, only)
--->
-
-<!ELEMENT haspref (icon?,(%pgiptype;))>
-<!ATTLIST haspref
-  %name_attr;
-  descr CDATA #IMPLIED
-  default CDATA #IMPLIED>
-
-<!ELEMENT hasprefs (haspref)*>
-<!ATTLIST hasprefs
-  prefcategory CDATA #IMPLIED>
-
-<!ELEMENT prefval (#PCDATA)>
-<!ATTLIST prefval
-  %name_attr;>
-
-<!-- menu items (incomplete) -->
-
-<!ENTITY % path_attr "
-  path CDATA #REQUIRED">
-
-<!ELEMENT menuadd (#PCDATA)>
-<!ATTLIST menuadd
-  path CDATA #IMPLIED
-  name CDATA #IMPLIED>
-
-<!ELEMENT menudel (#PCDATA)>
-<!ATTLIST menudel
-  path CDATA #IMPLIED
-  name CDATA #IMPLIED>
-
-<!--
-GUI configuration information: objects, types, and operations
-NB: the following object types have a fixed interpretation 
-in PGIP:  "comment", "thm", "theory", "file" 
--->
-
-<!ELEMENT guiconfig (objtype*,opn*)>
-
-<!ELEMENT objtype (icon?,hasprefs?,contains*)>
-<!ATTLIST objtype
-  %name_attr;
-  descr CDATA #IMPLIED>
-
-<!ENTITY % objtype_attr "
-  objtype CDATA #REQUIRED">
-
-<!-- the name of an objtype -->
-
-<!ELEMENT contains EMPTY>
-<!ATTLIST contains
-  %objtype_attr;>
-
-<!-- source types: a space separated list -->
-
-<!ENTITY % optrg "optrg?">
-
-<!--  -->
-
-<!ELEMENT opn (inputform?,opsrc,(%optrg;),opcmd)>
-<!ATTLIST opn
-  %name_attr;>
-
-<!ELEMENT optrg (#PCDATA)>
-
-<!ELEMENT opsrc (#PCDATA)>
-
-<!-- single target type, empty for proofstate -->
-
-<!ELEMENT opcmd (#PCDATA)>
-
-<!-- prover command, with printf-style "%1"-args -->
-
-<!-- interactive operations - require some input -->
-
-<!ELEMENT inputform (field)+>
-
-<!--
-a field has a PGIP config type (int, string, bool, choice(c1...cn))
-and a name; under that name, it will be substituted into the command
-Ex. field name=number  opcmd="rtac %1 %number"
--->
-
-<!ELEMENT field ((%pgiptype;),prompt)>
-<!ATTLIST field
-  %name_attr;>
-
-<!ELEMENT prompt (#PCDATA)>
-
-<!--
-identifier tables: these list known items of particular objtype.
-Might be used for completion or menu selection, and inspection.
-May have a nested structure (but objtypes do not).
--->
-
-<!ELEMENT setids (idtable)>
-
-<!-- (with an empty idtable, clear table) -->
-
-<!ELEMENT addids (idtable)>
-
-<!ELEMENT delids (idtable)>
-
-<!ENTITY % displaytext "(#PCDATA|pgml)*">
-
-<!-- give value of some identifier (response to showid) -->
-
-<!ELEMENT idvalue %displaytext;>
-<!ATTLIST idvalue
-  %name_attr;
-  %objtype_attr;>
-
-<!ELEMENT idtable (identifier|idtable)*>
-<!ATTLIST idtable
-  %objtype_attr;>
-
-<!ELEMENT identifier (#PCDATA)>
-
-<!--
-prover information: 
-name, description, version, homepage, 
-welcome message, docs available
--->
-
-<!ELEMENT proverinfo (welcomemsg?,icon?,helpdoc*)>
-<!ATTLIST proverinfo
-  %name_attr;
-  descr CDATA #IMPLIED
-  version CDATA #IMPLIED
-  url CDATA #IMPLIED>
-
-<!ELEMENT welcomemsg (#PCDATA)>
-
-<!ENTITY % url_attr "
-  url CDATA #REQUIRED">
-
-<!-- FIXME: schema for URL? -->
-
-<!--
-helpdoc: advertise availability of some documentation, given a canonical
-name, textual description, and URL or viewdoc argument.
-
--->
-
-<!ELEMENT helpdoc (#PCDATA)>
-<!ATTLIST helpdoc
-  %name_attr;
-  %descr_attr;
-  url CDATA #IMPLIED>
-
-<!-- deactivate use of symbols in PGML output -->
-
-<!ELEMENT proverinit EMPTY>
-
-<!ELEMENT proverexit EMPTY>
-
-<!ELEMENT startquiet EMPTY>
-
-<!ELEMENT stopquiet EMPTY>
-
-<!ELEMENT pgmlsymbolson EMPTY>
-
-<!ELEMENT pgmlsymbolsoff EMPTY>
-
-<!-- result of a <unparsecmds> request (see later) -->
-
-<!ELEMENT ready EMPTY>
-
-<!ENTITY % displayarea "message|display">
-
-<!-- the main display area (goals buffer) -->
-
-<!ELEMENT cleardisplay EMPTY>
-<!ATTLIST cleardisplay
-  area (%displayarea;|all) #REQUIRED>
-
-<!-- grammar for displayed text  -->
-
-<!ELEMENT normalresponse %displaytext;>
-<!ATTLIST normalresponse
-  area (%displayarea;) #REQUIRED
-  category CDATA #IMPLIED
-  urgent (y) #IMPLIED>
-
-<!ENTITY % fatality "nonfatal|fatal|panic">
-
-<!-- degree of errors -->
-
-<!ELEMENT errorresponse %displaytext;>
-<!ATTLIST errorresponse
-  fatality (%fatality;) #REQUIRED
-  location CDATA #IMPLIED
-  locationline CDATA #IMPLIED
-  locationcolumn CDATA #IMPLIED>
-
-<!ELEMENT scriptinsert (#PCDATA)>
-
-<!-- metainformation is an extensible place to put system-specific information -->
-
-<!ELEMENT value (#PCDATA)>
-<!ATTLIST value
-  name CDATA #IMPLIED>
-
-<!-- generic value holder -->
-
-<!ELEMENT metainforesponse (value)*>
-<!ATTLIST metainforesponse
-  infotype CDATA #REQUIRED>
-
-<!-- re-open previously postponed proof, outdating dependent theorems -->
-
-<!ENTITY % thmname_attr "
-  thmname CDATA #REQUIRED">
-
-<!-- theorem names -->
-
-<!ENTITY % aname_attr "
-  aname CDATA #REQUIRED">
-
-<!-- anchors in proof text -->
-
-<!ELEMENT opengoal (#PCDATA)>
-<!ATTLIST opengoal
-  %thmname_attr;>
-
-<!-- text is theorem to be proved -->
-
-<!ELEMENT proofstep (#PCDATA)>
-<!ATTLIST proofstep
-  aname CDATA #IMPLIED>
-
-<!-- text is proof command -->
-
-<!ELEMENT undostep EMPTY>
-
-<!ELEMENT closegoal EMPTY>
-<!ATTLIST closegoal
-  %thmname_attr;>
-
-<!ELEMENT abortgoal EMPTY>
-<!ATTLIST abortgoal
-  %thmname_attr;>
-
-<!ELEMENT giveupgoal EMPTY>
-<!ATTLIST giveupgoal
-  %thmname_attr;>
-
-<!ELEMENT postponegoal EMPTY>
-<!ATTLIST postponegoal
-  %thmname_attr;>
-
-<!ELEMENT forget EMPTY>
-<!ATTLIST forget
-  thyname CDATA #IMPLIED
-  aname CDATA #IMPLIED>
-
-<!ELEMENT restoregoal EMPTY>
-<!ATTLIST restoregoal
-  %thmname_attr;>
-
-<!ELEMENT comment (#PCDATA)>
-
-<!ELEMENT litcomment (#PCDATA)>
-
-<!-- request some on-line help (prover-specific arg) -->
-
-<!ENTITY % thyname_attr "
-  thyname CDATA #REQUIRED">
-
-<!-- theory name -->
-
-<!ELEMENT askids EMPTY>
-<!ATTLIST askids
-  thyname CDATA #IMPLIED
-  %objtype_attr;>
-
-<!ELEMENT showid EMPTY>
-<!ATTLIST showid
-  thyname CDATA #IMPLIED
-  %objtype_attr;
-  %name_attr;>
-
-<!ELEMENT setid (setpref*,obvalue)>
-<!ATTLIST setid
-  %name_attr;
-  %objtype_attr;>
-
-<!ELEMENT obvalue (#PCDATA)>
-
-<!-- text constructed with opcmds -->
-
-<!--
-NB: parse/unparsing needs only be supported for "proper" proof commands,
-which may appear in proof texts.
--->
-
-<!ENTITY % properscriptcmd "%properproofcmd;|%properfilecmd;|setid">
-
-<!ELEMENT parsescript (#PCDATA)>
-
-<!ELEMENT parseresult (%properscriptcmd;)*>
-
-<!ELEMENT unparsecmds (%properscriptcmd;)*>
-
-<!ELEMENT unparseresult (#PCDATA)>
-
-<!ELEMENT showproofstate EMPTY>
-
-<!ELEMENT showctxt EMPTY>
-
-<!ELEMENT searchtheorems (#PCDATA)>
-
-<!ELEMENT setlinewidth (#PCDATA)>
-
-<!ELEMENT viewdoc (#PCDATA)>
-
-<!-- prover informs interface a particular file is outdated -->
-
-<!--
-Below, url_attr will often be a file URL.  
-We assume for now that the prover and interface are running on same
-filesystem
--->
-
-<!ATTLIST changecwd
-  dir CDATA #REQUIRED>
-
-<!-- Unix directory name  -->
-
-<!ELEMENT opentheory (#PCDATA)>
-<!ATTLIST opentheory
-  %thyname_attr;>
-
-<!ELEMENT closetheory EMPTY>
-<!ATTLIST closetheory
-  %thyname_attr;>
-
-<!ELEMENT aborttheory EMPTY>
-<!ATTLIST aborttheory
-  %thyname_attr;>
-
-<!ELEMENT retracttheory EMPTY>
-<!ATTLIST retracttheory
-  %thyname_attr;>
-
-<!--
-FIXME: maybe add a command to ask prover for the file corresponding
-to some theory (prover searches it's search path / cwd).
--->
-
-<!ELEMENT loadfile EMPTY>
-<!ATTLIST loadfile
-  %url_attr;>
-
-<!ELEMENT openfile EMPTY>
-<!ATTLIST openfile
-  %url_attr;>
-
-<!ELEMENT closefile EMPTY>
-<!ATTLIST closefile
-  %url_attr;>
-
-<!ELEMENT abortfile EMPTY>
-<!ATTLIST abortfile
-  %url_attr;>
-
-<!ELEMENT changecwd EMPTY>
-
-<!ELEMENT informfileloaded EMPTY>
-<!ATTLIST informfileloaded
-  %thyname_attr;
-  %url_attr;>
-
-<!ELEMENT informfileretracted EMPTY>
-<!ATTLIST informfileretracted
-  %thyname_attr;
-  %url_attr;>
diff --git a/html/Kit/dtd/pgip.rnc b/html/Kit/dtd/pgip.rnc
deleted file mode 100644
index 0555dc21..00000000
--- a/html/Kit/dtd/pgip.rnc
+++ /dev/null
@@ -1,411 +0,0 @@
-# 
-# RELAX NG Schema for PGIP, the Proof General Interface Protocol                   
-# 
-# Authors:  David Aspinall, LFCS, University of Edinburgh       
-#           Christoph Lueth, University of Bremen       
-#
-# Version: pgip.rnc,v 1.37 2003/09/25 09:11:49 da Exp    
-# 
-# Status:  Experimental.                                           
-# For additional commentary, see the Proof General Kit white paper,
-# available from http://www.proofgeneral.org/kit
-# 
-# Advertised version: 1.0
-#
-
-
-
-include "pgml.rnc"                           # include PGML grammar
-
-# ========== PGIP MESSAGES ==========
-
-start = pgip | pgips                         # pgips is the type of a log between
-                                             # two components.
-
-pgip = element pgip {                        # A PGIP packet contains:
-   pgip_attrs,                               # attributes with header information;
-   (provermsg                                # either a message sent TO the prover,
-     | kitmsg)}                              # or an interface message
-
-pgips = element pgips { pgip+ }
-
-pgip_attrs =
-  attribute origin { text }?,                # name of sending PGIP component
-  attribute id { text },                     # session identifier for component process
-  attribute class { pgip_class },            # general categorization of message
-  attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to
-  attribute refid { text }?,                 # message id this message responds to
-  attribute seq { xsd:positiveInteger }      # sequence number of this message
-
-
-pgip_class = "pa"  # for a message sent TO the proof assistant
-           | "pg"  # for a message sent TO proof general
-
-provermsg = 
-   proverconfig    # query Prover configuration, triggering interface configuration
- | provercontrol   # control some aspect of Prover
- | proofcmd        # issue a proof command 
- | proofctxt	   # issue a context command
- | filecmd         # issue a file command
-
-kitmsg = 
-   kitconfig       # messages to configure the interface 
- | proveroutput    # output messages from the prover, usually display in interface
- | fileinfomsg     # information messages concerning 
-
-
-
-
-#  ========== PROVER CONFIGURATION ==========
-
-proverconfig =      
-   askpgip         # what version of PGIP do you support?
- | askpgml         # what version of PGML do you support?
- | askconfig       # tell me about objects and operations
- | askprefs        # what preference settings do you offer?
- | setpref         # please set this preference value 
- | getpref         # please tell me this preference value
-
-name_attr = attribute name { token }            # identifiers must be XML tokens
-
-
-prefcat_attr = attribute prefcategory { text}   # e.g. "expert", "internal", etc.
-                                                # could be used for tabs in dialog
-
-askpgip   = element askpgip   { empty }
-askpgml   = element askpgml   { empty }
-askconfig = element askconfig { empty }
-askprefs  = element askprefs  { prefcat_attr? }
-setpref   = element setpref   { name_attr, prefcat_attr?, text }
-getpref   = element getpref   { name_attr, prefcat_attr? }
-
- 
-
-#  ========== INTERFACE CONFIGURATION ==========
-
-kitconfig =        
-    usespgip       # I support PGIP, version ..
-  | usespgml       # I support PGML, version ..
-  | pgmlconfig     # configure PGML symbols
-  | proverinfo	   # Report assistant information
-  | hasprefs       # I have preference settings ...
-  | prefval        # the current value of a preference is
-  | guiconfig      # configure the following object types and operations
-  | setids	   # inform the interface about some known objects
-  | addids         # add some known identifiers
-  | delids         # retract some known identifers
-  | idvalue	   # display the value of some identifier
-  | menuadd        # add a menu entry
-  | menudel        # remove a menu entry
-
-# version reporting
-version_attr  = attribute version { text }
-usespgml = element usespgml  { version_attr }
-usespgip = element usespgip  { version_attr }
-
-# PGML configuration
-pgmlconfig = element pgmlconfig { pgmlconfigure+ }
-
-# Types for config settings: corresponding data values should conform
-# to representation for corresponding XML Schema 1.0 Datatypes.
-# (This representation is verbose but helps for error checking later)
-
-pgiptype   = pgipbool | pgipint | pgipstring | pgipchoice
-pgipbool   = element pgipbool { empty }
-
-pgipint    = element pgipint  { min_attr?, max_attr?, empty }
-min_attr   = attribute min { xsd:integer }
-max_attr   = attribute max { xsd:integer }
-pgipstring = element pgipstring { empty }
-pgipchoice = element pgipchoice { pgipchoiceitem+ }
-pgipchoiceitem = element pgipchoiceitem { text }
-
-icon  = element icon { xsd:base64Binary }  # image data for an icon
-
-# preferences
-default_attr = attribute default { text }
-descr_attr   = attribute descr { text }
-
-# icons for preference recommended size: 32x32 
-# top level preferences: may be used in dialog for preference setting
-# object preferences: may be used as an "emblem" to decorate 
-# object icon (boolean preferences with default false, only)
-haspref = element haspref  { 
-   name_attr, descr_attr?, 
-   default_attr?, icon?,
-   pgiptype
-}
-
-hasprefs = element hasprefs { prefcat_attr?, haspref* }
-
-prefval = element prefval  { name_attr, text }
-
-# menu items (incomplete)
-path_attr = attribute path { text }
-
-menuadd = element menuadd  { path_attr?, name_attr?, text }
-menudel = element menudel  { path_attr?, name_attr?, text }
-
-
-# GUI configuration information: objects, types, and operations
-# NB: the following object types have a fixed interpretation 
-# in PGIP:  "comment", "thm", "theory", "file" 
-
-guiconfig =
-  element guiconfig { objtype*, opn* }
-
-objtype = element objtype { name_attr, descr_attr?, icon?, hasprefs?, contains* }
-
-objtype_attr = attribute objtype { token }           # the name of an objtype
-contains = element contains { objtype_attr, empty }  # 
-
-opn   = element opn { name_attr, inputform?, opsrc, optrg, opcmd }
-
-opsrc = element opsrc { list { token* } }  # source types: a space separated list
-optrg = element optrg { token }?    # single target type, empty for proofstate
-opcmd = element opcmd { text }      # prover command, with printf-style "%1"-args
-
-# interactive operations - require some input
-inputform = element inputform { field+ }  
-
-# a field has a PGIP config type (int, string, bool, choice(c1...cn))
-# and a name; under that name, it will be substituted into the command
-# Ex. field name=number  opcmd="rtac %1 %number"
-
-field = element field { 
-   name_attr, pgiptype,
-   element prompt { text }
-}
-
-# identifier tables: these list known items of particular objtype.
-# Might be used for completion or menu selection, and inspection.
-# May have a nested structure (but objtypes do not).
-
-setids  = element setids { idtable }	# (with an empty idtable, clear table)
-addids  = element addids { idtable }
-delids  = element delids { idtable }
-
-# give value of some identifier (response to showid)
-idvalue = element idvalue		
-   {  name_attr, objtype_attr, displaytext }
-
-idtable    = element idtable { objtype_attr, (identifier | idtable)* }
-identifier = element identifier { token }
-
-# prover information: 
-# name, description, version, homepage, 
-# welcome message, docs available
-proverinfo = element proverinfo 
-   { name_attr, descr_attr?, version_attr?, url_attr?,
-     welcomemsg?, icon?, helpdoc* }
-welcomemsg = element welcomemsg { text }
-url_attr   = attribute url { text } # FIXME: schema for URL?
-
-# helpdoc: advertise availability of some documentation, given a canonical
-# name, textual description, and URL or viewdoc argument.
-# 
-helpdoc    = element helpdoc { name_attr, descr_attr, url_attr?, text } # text is arg to "viewdoc"
-
-
-# ========== PROVER CONTROL ==========
-
-provercontrol = 
-   proverinit      # reset prover to its initial state
- | proverexit      # exit prover
- | startquiet      # stop prover sending proof state displays, non-urgent messages
- | stopquiet       # turn on normal proof state & message displays
- | pgmlsymbolson   # activate use of symbols in PGML output (input always understood)
- | pgmlsymbolsoff  # deactivate use of symbols in PGML output
-
-proverinit     = element proverinit { empty }  
-proverexit     = element proverexit { empty }
-startquiet     = element startquiet { empty }  
-stopquiet      = element stopquiet  { empty }  
-pgmlsymbolson  = element pgmlsymbolson { empty }
-pgmlsymbolsoff = element pgmlsymbolsoff { empty }
-
-
-# ========== GENERAL PROVER OUTPUT/RESPONSES ==========
-
-proveroutput =
-   ready                # prover is ready for input
- | cleardisplay         # prover requests a display area to be cleared
- | proofstate	        # prover outputs the proof state
- | normalresponse       # prover outputs some display
- | errorresponse        # prover indicates an error condition, with error message
- | scriptinsert         # some text to insert literally into the proof script
- | metainforesponse     # prover outputs some other meta-information to interface
- | parseresult		# result of a <parsescript> request (see later)
- | unparseresult	# result of a <unparsecmds> request (see later)
-
-ready = element ready { empty }            
-
-displayarea = "message"                    # the message area (response buffer)
-            | "display"                    # the main display area (goals buffer)
-
-cleardisplay = 
-   element cleardisplay {
-      attribute area { 
-         displayarea | "all" } }           
-
-
-displaytext = (text | pgml)*               # grammar for displayed text 
-
-proofstate = 
-  element proofstate { displaytext }
-
-normalresponse =                           
-  element normalresponse { 
-    attribute area { displayarea },
-    attribute category { text }?,          # optional extra category (e.g. tracing/debug)
-    attribute urgent { "y" }?,             # indication that message must be displayed
-    displaytext 
-}
-
-fatality = "nonfatal" | "fatal" | "panic"  # degree of errors
-
-errorresponse = 
-   element errorresponse { 
-     attribute fatality { fatality },
-     attribute location { text }?,
-     attribute locationline { xsd:positiveInteger }?,
-     attribute locationcolumn { xsd:positiveInteger }?,
-     displaytext
-  }
-
-scriptinsert = element scriptinsert { text }
-
-
-# metainformation is an extensible place to put system-specific information
-
-value = element value { name_attr?, text }   # generic value holder
-
-metainforesponse = 
-   element metainforesponse { 
-      attribute infotype { text },      # categorization of data
-      value* }                          # data values
-
-
-# ========== PROOF CONTROL COMMANDS ==========
-
-proofcmd =
-    properproofcmd | improperproofcmd
-
-properproofcmd =
-    opengoal      # open a goal in ambient context
-  | proofstep     # a specific proof command (perhaps configured via opcmd) 
-  | closegoal     # complete & close current open proof (succeeds iff goal proven)
-  | giveupgoal    # close current open proof, record as proof obl'n  (sorry)  
-  | postponegoal  # close current open proof, retaining attempt in script (oops)
-  | comment	  # an ordinary comment: text ignored by prover
-  | litcomment    # a "literate" comment: text processed by prover, but no sidefx
-
-improperproofcmd =
-    undostep      # undo the last proof step issued in currently open goal 
-  | abortgoal     # give up on current open proof, close proof state, discard history
-  | forget        # forget a theorem (or named target), outdating dependent theorems
-  | restoregoal   # re-open previously postponed proof, outdating dependent theorems
-
-thmname_attr = attribute thmname { text }   # theorem names
-aname_attr   = attribute aname { text }     # anchors in proof text
-
-opengoal     = element opengoal { thmname_attr, text }   # text is theorem to be proved
-proofstep    = element proofstep { aname_attr?, text }   # text is proof command
-undostep     = element undostep { empty }
-
-closegoal    = element closegoal { empty }
-abortgoal    = element abortgoal { empty }
-giveupgoal   = element giveupgoal { empty }
-postponegoal = element postponegoal { empty }
-forget       = element forget { thyname_attr?, aname_attr? }
-restoregoal  = element restoregoal { thmname_attr }
-comment	     = element comment { text }
-litcomment   = element litcomment { text }
-
-
-# ========= PROOF CONTEXT/ETC COMMANDS ===========
-
-proofctxt =
-    askids	   # please tell me about identifiers (given objtype in a theory)
-  | showid	   # print value of an object
-  | bindid	   # extend current context with identifer assignment
-  | parsescript    # parse a raw proof script into proofcmds
-  | unparsecmds    # unprase proofcmds into raw proof script
-  | showproofstate # (re)display proof state (empty if outside a proof)
-  | showctxt	   # show proof context
-  | searchtheorems # search for theorems (prover-specific arguments)  
-  | setlinewidth   # set line width for printing
-  | viewdoc	   # request some on-line help (prover-specific arg)
-
-thyname_attr = attribute thyname { text }       # theory name
-
-askids = element askids  { thyname_attr?, objtype_attr }
-
-showid = element showid  { thyname_attr?, objtype_attr, name_attr }
-bindid = element setid   { name_attr, objtype_attr, setpref*, objval }
-objval = element obvalue { text }   # text constructed with opcmds
-
-
-# NB: parse/unparsing needs only be supported for "proper" proof commands,
-# which may appear in proof texts.
-
-properscriptcmd = properproofcmd | properfilecmd | bindid
-
-parsescript = element parsescript { text }
-parseresult = element parseresult { properscriptcmd* }
-
-unparsecmds   = element unparsecmds { properscriptcmd* }
-unparseresult = element unparseresult { text }
-
-showproofstate = element showproofstate { empty }
-showctxt       = element showctxt { empty }
-searchtheorems = element searchtheorems { text }
-setlinewidth   = element setlinewidth { xsd:positiveInteger }
-viewdoc	       = element viewdoc { text }
-
-
-# ========== THEORY/FILE HANDLING COMMANDS ==========
-
-filecmd =
-   properfilecmd | improperfilecmd
-
-properfilecmd =
-    opentheory      # begin construction of a new theory.  
-  | closetheory     # complete construction of the currently open theory
-
-improperfilecmd =
-    aborttheory     # abort currently open theory
-  | retracttheory   # retract a named theory
-  | openfile        # lock a file for constructing a proof text 
-  | closefile       # unlock a file, suggesting it has been processed
-  | abortfile       # unlock a file, suggesting it hasn't been processed
-  | loadfile        # load a file possibly containing theory definition(s)
-  | changecwd	    # change prover's working directory (or load path) for files
-
-fileinfomsg = 
-   informfileloaded       # prover informs interface a particular file is loaded
- | informfileretracted    # prover informs interface a particular file is outdated
-
-# Below, url_attr will often be a file URL.  
-# We assume for now that the prover and interface are running on same
-# filesystem
-
-dir_attr      = attribute dir { text }   # Unix directory name 
-
-opentheory    = element opentheory    { thyname_attr, text }
-closetheory   = element closetheory   { empty }
-aborttheory   = element aborttheory   { empty }
-retracttheory = element retracttheory { thyname_attr }
-
-# FIXME: maybe add a command to ask prover for the file corresponding
-# to some theory (prover searches it's search path / cwd).
-loadfile      = element loadfile      { url_attr }
-openfile      = element openfile      { url_attr }
-closefile     = element closefile     { empty }
-abortfile     = element abortfile     { empty }
-changecwd     = element changecwd     { dir_attr }
-
-informfileloaded = 
-   element informfileloaded    { thyname_attr, url_attr }
-informfileretracted =
-   element informfileretracted { thyname_attr, url_attr }
diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd
deleted file mode 100644
index fbdd9f7d..00000000
--- a/html/Kit/dtd/pgml.dtd
+++ /dev/null
@@ -1,120 +0,0 @@
-<?xml encoding="UTF-8"?>
-
-<!--
-
-RELAX NG Schema for PGML, the Proof General Markup Language
-
-Authors:  David Aspinall, LFCS, University of Edinburgh       
-          Christoph Lueth, University of Bremen	
-Version: pgml.dtd,v 1.12 2003/09/23 23:17:18 da Exp    
-
-Status:  Complete but experimental version.
-
-For additional commentary, see the Proof General Kit white paper, 
-available from http://www.proofgeneral.org/kit 
-
-Advertised version: 1.0
-
--->
-
-<!ENTITY % pgml_version_attr "
-  version NMTOKEN #REQUIRED">
-
-<!ELEMENT pgml (statedisplay|termdisplay|information|warning|error)*>
-<!ATTLIST pgml
-  version NMTOKEN #IMPLIED>
-
-<!ENTITY % nonactionitem "term|type|atom|sym">
-
-<!ENTITY % termitem "action|%nonactionitem;">
-
-<!ENTITY % pgml_name_attr "
-  name CDATA #REQUIRED">
-
-<!ENTITY % kind_attr "
-  kind CDATA #REQUIRED">
-
-<!ENTITY % systemid_attr "
-  systemid CDATA #REQUIRED">
-
-<!ELEMENT statedisplay (#PCDATA|%termitem;|statepart)*>
-<!ATTLIST statedisplay
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED
-  systemid CDATA #IMPLIED>
-
-<!ENTITY % pgmltext "(#PCDATA|%termitem;)*">
-
-<!ELEMENT information %pgmltext;>
-<!ATTLIST information
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!ELEMENT warning %pgmltext;>
-<!ATTLIST warning
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!ELEMENT error %pgmltext;>
-<!ATTLIST error
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!ELEMENT statepart %pgmltext;>
-<!ATTLIST statepart
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!ELEMENT termdisplay %pgmltext;>
-<!ATTLIST termdisplay
-  name CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!ENTITY % pos_attr "
-  pos CDATA #REQUIRED">
-
-<!ELEMENT term %pgmltext;>
-<!ATTLIST term
-  pos CDATA #IMPLIED
-  kind CDATA #IMPLIED>
-
-<!-- maybe combine this with term and add extra attr to term? -->
-
-<!ELEMENT type %pgmltext;>
-<!ATTLIST type
-  kind CDATA #IMPLIED>
-
-<!ELEMENT action (#PCDATA|%nonactionitem;)*>
-<!ATTLIST action
-  kind CDATA #IMPLIED>
-
-<!ENTITY % fullname_attr "
-  fullname CDATA #REQUIRED">
-
-<!ELEMENT atom (#PCDATA)>
-<!ATTLIST atom
-  kind CDATA #IMPLIED
-  fullname CDATA #IMPLIED>
-
-<!ENTITY % symname_attr "
-  name CDATA #REQUIRED">
-
-<!ELEMENT sym EMPTY>
-<!ATTLIST sym
-  %symname_attr;>
-
-<!-- configuring PGML -->
-
-<!ENTITY % pgmlconfigure "symconfig">
-
-<!-- inform symbol support (I/O) for given sym -->
-
-<!ENTITY % asciialt "
-  alt CDATA #REQUIRED">
-
-<!-- understanding of ASCII alt for given sym -->
-
-<!ELEMENT symconfig EMPTY>
-<!ATTLIST symconfig
-  %symname_attr;
-  alt CDATA #IMPLIED>
diff --git a/html/Kit/dtd/pgml.rnc b/html/Kit/dtd/pgml.rnc
deleted file mode 100644
index 4e5c8053..00000000
--- a/html/Kit/dtd/pgml.rnc
+++ /dev/null
@@ -1,71 +0,0 @@
-# 
-# RELAX NG Schema for PGML, the Proof General Markup Language
-# 
-# Authors:  David Aspinall, LFCS, University of Edinburgh       
-#           Christoph Lueth, University of Bremen	
-# Version: pgml.rnc,v 1.5 2003/09/23 23:12:47 da Exp    
-# 
-# Status:  Complete but experimental version.
-# 
-# For additional commentary, see the Proof General Kit white paper, 
-# available from http://www.proofgeneral.org/kit 
-# 
-# Advertised version: 1.0
-# 
-
-pgml_version_attr = attribute version { xsd:NMTOKEN }
-
-pgml =
-  element pgml {
-    pgml_version_attr?,
-    (statedisplay | termdisplay | information | warning | error)*
-  }
-
-termitem      = action | nonactionitem
-nonactionitem = term | pgmltype | atom | sym
-
-pgml_name_attr = attribute name { text }
-
-kind_attr = attribute kind { text }
-systemid_attr = attribute systemid { text }
-
-statedisplay =
-  element statedisplay {
-    pgml_name_attr?, kind_attr?, systemid_attr?,
-     (text | termitem | statepart)*
-  }
-
-pgmltext = (text | termitem)*
-
-information =
-  element information { pgml_name_attr?, kind_attr?, pgmltext }
-
-warning     = element warning     { pgml_name_attr?, kind_attr?, pgmltext }
-error       = element error       { pgml_name_attr?, kind_attr?, pgmltext }
-statepart   = element statepart   { pgml_name_attr?, kind_attr?, pgmltext }
-termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext }
-
-pos_attr = attribute pos { text }
-
-term = element term { pos_attr?, kind_attr?, pgmltext }
-
-# maybe combine this with term and add extra attr to term?
-pgmltype = element type { kind_attr?, pgmltext }
-
-action = element action { kind_attr?, (text | nonactionitem)* }
-
-fullname_attr = attribute fullname { text }
-atom = element atom { kind_attr?, fullname_attr?, text }
-
-
-## Symbols
-
-symname_attr = attribute name { text }
-sym	     = element sym { symname_attr }
-
-# configuring PGML
-
-pgmlconfigure = symconfig		# inform symbol support (I/O) for given sym
-asciialt = attribute alt { text }	# understanding of ASCII alt for given sym
-
-symconfig = element symconfig { symname_attr, asciialt? }
diff --git a/html/Makefile b/html/Makefile
deleted file mode 100644
index 182a7a17..00000000
--- a/html/Makefile
+++ /dev/null
@@ -1,37 +0,0 @@
-#
-# Publish files to Informatics web server.
-#
-# Requires permissions in /group/project/proofgeneral
-#
-# $Id$
-#
-# FIXME: we want to have --delete and --delete-excluded in sync,
-# but yet preserve ProofGeneral-*  (distribs).  How to do that?
-# Might be better to put distribs elsewhere.
-
-PWD=`pwd`
-IGNOREDWEBFILES=*~,*.NOEXPORT,CVS/,/test/,/test/*,/tmp,/tmp/*,/Makefile,.cvsignore
-
-# Run rsync using ssh
-# --cvs-exclude: auto ignore files in the same way CVS does [exc. .cvsignore]
-# --include=ProofGeneral-* to avoid deleting archives
-# --delete-excluded
-EXCLUDEFILE=.tmp-rsync-excludes
-RSYNC=rsync -e ssh -auv --safe-links --force  --exclude-from=${EXCLUDEFILE} --include='releases-emacs' --exclude="/${EXCLUDEFILE}" --cvs-exclude
-
-DESTWEB=ssh.inf.ed.ac.uk:/group/project/proofgeneral/web
-DESTCGI=ssh.inf.ed.ac.uk:/group/project/proofgeneral/cgi
-
-default: pub
-
-excludes:
-	echo '${IGNOREDWEBFILES}'  | sed 's/,/\n/g' > ${EXCLUDEFILE}
-
-test:	excludes
-	${RSYNC} --exclude=/cgi/ -n ${PWD}/ ${DESTWEB} 
-#	${RSYNC} -n ${PWD}/cgi/  ${DESTCGI}
-
-pub:	excludes
-	${RSYNC} --exclude=/cgi/ ${PWD}/ ${DESTWEB} 
-#	${RSYNC} ${PWD}/cgi/ ${DESTCGI}
-
diff --git a/html/ProofGeneralPortrait.eps.gz b/html/ProofGeneralPortrait.eps.gz
deleted file mode 100644
index 97feb1a4..00000000
--- a/html/ProofGeneralPortrait.eps.gz
+++ /dev/null
diff --git a/html/about b/html/about
deleted file mode 100644
index a58717d8..00000000
--- a/html/about
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/about.html b/html/about.html
deleted file mode 100644
index 2c8e03db..00000000
--- a/html/about.html
+++ /dev/null
@@ -1,54 +0,0 @@
-<h2>Contact information</h2>
-
-<p>
-Have you any questions, comments, or suggestions about Proof General?
-<br>
-Send us a message using <a href="feedback">this form</a>
-or by email to 
-<?php mlinktxt($project_feedback, "$project_feedback"); ?>.
-<br>
-Receive announcements and discuss Proof General on 
-our <a href="mailinglist">mailing
-list</a>.
-</p>
-
-<h2>About the Proof General project</h2>
-<p>
-The forefather of Proof General was LEGO mode, begun in 1994 at the <a
-href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a> by Thomas Kleymann.  LEGO
-mode was an Emacs-based front end for LEGO similar to David Aspinall's
-<a href="http://homepages.inf.ed.ac.uk/da/Isamode">Isamode</a>,
-developed at the LFCS since 1992.  After 1994, implementations of
-proof-by-pointing and script management were added to LEGO mode, and
-the code was made generic.  The generic basis was developed by
-Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall.
-The current authors and maintainers of the various instantiations of
-Proof General are mentioned on the 
-<a href="main">front page</a>.
-</p>
-<p> 
-The Proof General project was coordinated until October 1998 by
-Thomas Kleymann, and since then by David Aspinall.  The project has
-benefited from funding by 
-<!-- this link is broken: <a href="http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html"> -->
-EPSRC, 
-<!-- (Applications of a Type Theory based Proof Assistant) -->
-<!-- </a>, -->
-the <a
-href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>,
-and the <a href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a>.
-</p>
-
-<p>
-David Aspinall designed the web pages and graphics for Proof General.
-<br>
-Check the <a href="gallery">gallery</a> for more publicity
-pictures!
-</p>
-<p>
-For more on the history of the development of
-the Proof General program, see the 
-<?php htmlshow("ProofGeneral/doc/ProofGeneral_1.html#SEC3","manual preface.","","html") ?>
-</p>
-
-<?php include('links.html') ?>
diff --git a/html/adaptingman b/html/adaptingman
deleted file mode 100644
index 74a3152c..00000000
--- a/html/adaptingman
+++ /dev/null
@@ -1,3 +0,0 @@
-<?php require('functions.php3');
-      hack_html("ProofGeneral/doc/PG-adapting_toc.html","Proof General adapting manual");
-?>
diff --git a/html/components b/html/components
deleted file mode 100644
index 7f600582..00000000
--- a/html/components
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('components.html'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/components.html b/html/components.html
deleted file mode 100644
index 6d6a73a2..00000000
--- a/html/components.html
+++ /dev/null
@@ -1,72 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Standalone Components"); 
-  ?>
-
-<p> As part of the Proof General project, some components have been
-developed which might be useful in a wider context.  They are
-presented on this page.
-</p>
-
-<p>As usual with free software, these programs
-come with no guarantees of any sort.
-Nonetheless, please <a href="feedback">contact us</a> with
-any comments, suggestions, or problems.
-</p>
-
-<h2>Spans: Emacs and XEmacs compatibility library for overlays/extents</h2>
-
-<p>
-<i>Spans</i> are an abstraction of XEmacs <i>extents</i> used to help
-bridge the gulf between GNU Emacs and XEmacs.  In GNU Emacs, spans are
-implemented using <i>overlays</i>.  
-</p>
-<p>
-The library consists of three Emacs lisp files,
-<ul>
-<li><a href="ProofGeneral-latest/generic/span-extent.el">span-extent.el</a>
-</li>
-<li><a href="ProofGeneral-latest/generic/span-overlay.el">span-overlay.el</a>
-</li>
-<li><a href="ProofGeneral-latest/generic/span.el">span.el</a> 
-(which simply loads one of the above)
-</li>
-</ul>
-which implement a common interface for overlays/extents.
-This library was originally implemented by Healfdene Goguen.
-</p>
-<p>
-See the files for further documentation, and 
-<a href="htmlshow.php?title=Proof+General+adapting+manual&file=ProofGeneral%2Fdoc%2FPG-adapting_13.html#SEC40">section 12.1</a>
-of the <a href="adaptingman">Proof General adapting manual</a>
-for more details.
-</p>
-
-
-<h2>Docstring magic: Elisp documentation to TeXinfo extraction</h2>
-
-<p>
-This package generates <a
-href="http://www.gnu.org/directory/texinfo.html">Texinfo</a> source
-fragments from Emacs 
-<!-- WARNING: next URL subject to change with elisp ref man changes!! -->
-<a href="http://www.gnu.org/manual/elisp/html_node/elisp_374.html#SEC374">documentation strings</a> which are embedded in Emacs lisp source and the 
-running interpreter.  This avoids documenting functions
-and variables in more than one place, and automatically adds Texinfo
-markup to docstrings.  It's a bit like <tt>javadoc</tt> for Emacs
-Lisp, except that you must write a skeleton <tt>texi</tt> file which
-contains magic comments mentioning the function or variable names you
-want documented.  </p> <p> The package consists of one file: <ul>
-<li><a
-href="ProofGeneral-latest/generic/texi-docstring-magic.el">texi-docstring-magic.el</a></li>
-</ul> which contains documentation and usage hints.  For an extensive
-example of it's use, see the <a
-href="ProofGeneral-latest/doc/PG-adapting.texi">source</a> for the <a
-href="adaptingman">PG adapting manual</a>.  </p>
-
-<hr>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/counter.php3 b/html/counter.php3
deleted file mode 100644
index 0ea4593d..00000000
--- a/html/counter.php3
+++ /dev/null
@@ -1,50 +0,0 @@
-<?php
-/*
- * Increment an access counter.
- * David Aspinall, June 1999.
- *
- * $Id$
- *
- */
-
-$counterFile = "counter.txt";
-$counterStart = "counterstart.txt";
-$maxlen = 10;
-
-// NB: probably have trouble with permissions 
-//     if file doesn't exist already, so start with
-//     empty files made with touch.
-
-// Here's how to cause it to be initialized:
-//
-//  rm -f counter.txt counterstart.txt
-//  touch counter.txt counterstart.txt
-//  chmod o+w counter.txt counterstart.txt
-//
-
-if (is_readable($counterFile) && is_writeable($counterFile)) {
-  $fp   = fopen($counterFile,"r+");
-  if (filesize($counterFile)<1) {
-     // Start counter, write a timestamp.
-     $num = 1;
-     if (is_readable($counterStart) && is_writeable($counterStart)) {
-	$fps = fopen($counterStart,"w");
-        fputs($fps,time());
-        fclose($fps);
-        print "<!-- Hit counter initialized. -->";
-     } else {
-        print "<!-- Hit counter initialized, but timestamp could not be set -->";
-     };
-  } else {
-     $num  = fgets($fp,$maxlen);
-     $num += 1;
-     print "<!-- Hit counter: $num -->";
-  };
-  rewind($fp);
-  fputs($fp,$num);
-  fclose($fp);
-} else {
-  print "<!-- Hit counter file $counterFile cannot be accessed. -->";
-};
-?>
-
diff --git a/html/devel b/html/devel
deleted file mode 100644
index a58717d8..00000000
--- a/html/devel
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/devel.html b/html/devel.html
deleted file mode 100644
index c468dc47..00000000
--- a/html/devel.html
+++ /dev/null
@@ -1,135 +0,0 @@
-<h2>Development Information</h2>
-<p>
-Proof General follows an open development method.  
-<br>
-We encourage code contributions, suggestions, and bug reports, from all
-users.
-</p>
-
-<ul>
-<li>
-Download the latest <a href="develdownload.html">development release: 
-<!-- WARNING!  Line below automatically edited by makefile. -->
- <b>ProofGeneral-3.5pre040207</b></a>
-<!-- end WARNING -->
-<br>
-or <a href="ProofGeneral">browse</a> the development distribution.
- <br>
-Check the 
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<?php fileshow("ProofGeneral-3.5pre040207/CHANGES","CHANGES"); ?> file
-<!-- End Warning. -->
-for a summary of changes since the last stable version.
-</li>
-</ul>
-
-<ul>
-<li>
-<b>New!</b>  The Proof General CVS repository is available by
-anonymous CVS.  Login with:
-<blockquote>
-      cvs -d :pserver:anon@cvs.inf.ed.ac.uk:/disk/cvs/proofgen login
-</blockquote>
-and use the password <tt>anon</tt>.  Then you can check out
-the CVS with:
-<blockquote>
-      cvs -d :pserver:anon@cvs.inf.ed.ac.uk:/disk/cvs/proofgen checkout ProofGeneral
-</blockquote>
-For more information, see the file <tt>etc/cvs-tips.txt</tt> in the
-repository.  (If you want to be an "official" developer and
-have write access to the CVS repository, 
-<a href="feedback">ask here first</a>).
-</li>
-</ul>
-
-<ul>
-<li>
-Read about ideas for the <a href="kit">Proof General Kit</a>
-here.
-</li>
-</ul>
-
-<ul>
-<li>
-Take a look at some Proof General <a href="projects.html">project proposals</a>.
-</li>
-</ul>
-
-
-<ul>
-<li>
-Read the 
-developer's 
-<?php fileshow("ProofGeneral-3.5pre040207/etc/README.devel","README file"); ?>, 
-with development hints and tips.
-</li>
-</ul>
-
-
-<ul>
-<li>
-Read the brief list of planned 
-<?php fileshow("ProofGeneral-3.5pre040207/TODO","things to do "); ?> 
-for Proof General.
-</ul>
-<ul>
-<li>
-<a name="lowleveltodo">See our current low-level lists of things to do</a>, 
-for the
-<!-- WARNING!  Lines below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.5pre040207/todo","generic base"); ?>, 
-  <br>
-  and for each prover:
-   <?php fileshow("ProofGeneral-3.5pre040207/lego/todo","lego to do"); ?>,
-   <?php fileshow("ProofGeneral-3.5pre040207/coq/todo","coq to do"); ?>,
-   <?php fileshow("ProofGeneral-3.5pre040207/isa/todo","isa to do"); ?>,
-   <?php fileshow("ProofGeneral-3.5pre040207/isar/todo","isar to do"); ?>,
-   <?php fileshow("ProofGeneral-3.5pre040207/hol98/todo","hol to do"); ?>.
-<!-- end WARNING -->
-</li>
-</ul>
-
-<ul>
-<li>
-See Proof General's <a href="components">standalone components</a>
-which can be used in other programs.
-</li>
-</ul>
-
-
-
-<!-- <ul> -->
-<!-- <li> -->
-<!-- Browse source files from the current pre-release: -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-site.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-config.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-script.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-shell.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-toolbar.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-syntax.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-splash.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.5pre040207/generic/proof-easy-config.el") ?>. -->
-<!-- </ul> -->
-
-
-<ul>
-<li>
-<?php hlink("feedback","Send us a message ","Feedback form")?>
-about any development issues.
-</li>
-</ul>
-
-<h2><a name="develmail">Developers Mailing List</a></h2>
-
-<p>
-We have a mailing list for developers, at
-<a href="mailto:proofgeneral-devel@inf.ed.ac.uk">proofgeneral-devel@inf.ed.ac.uk</a>.
-<br>
-Posting is restricted to list members.
-To subscribe (or unsubscribe), 
-visit 
-<a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral-devel">this 
-web page</a>.
-</p>
-
diff --git a/html/develdownload b/html/develdownload
deleted file mode 100644
index 4c9b3b01..00000000
--- a/html/develdownload
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('develdownload.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/develdownload.html b/html/develdownload.html
deleted file mode 100644
index 4c9b3b01..00000000
--- a/html/develdownload.html
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('develdownload.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/develdownload.php b/html/develdownload.php
deleted file mode 100644
index 19af60f8..00000000
--- a/html/develdownload.php
+++ /dev/null
@@ -1,152 +0,0 @@
-<!-- -*- html -*- -->
-<?php  
-  require('functions.php3');
-  small_header("Proof General Development Release"); 
-  ?>
-
-
-<p>
-<a href="#prerel">Below</a> is the latest pre-release of Proof General,
-made available for those who wish to test the latest features or bug
-fixes.  For developers, this release is also available as a 
-<a href="#devel">complete CVS snapshot</a> (further below), which
-includes files not needed for the running program.
-</p>
-<p>
-Pre-releases of Proof General may be buggy as we add new features and
-experiment with them.  Nonetheless, we welcome bug reports.  But
-please make sure you are using the latest pre-release before
-reporting problems.
-</p>
-<p>
-Please <a href="register">register</a> if you haven't done so already.
-</p>
-
-
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<h2><a name="doc">Manual for ProofGeneral-3.5pre040207</a></h2>
-<!-- End Warning. -->
-<p>
-The manual included with the pre-release may be
-updated from that of the 
-<a href="doc">last stable release</a>.
-</p>
-<p>
-Here is the pre-release documentation: the user manual in
-<?php htmlshow("ProofGeneral-latest/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>,
-<?php download_link("ProofGeneral-latest/doc/ProofGeneral.ps.gz", "ps") ?> 
-or  
-<?php download_link("ProofGeneral-latest/doc/ProofGeneral.pdf", "pdf") ?>,
-and the adapting manual, in
-<?php htmlshow("ProofGeneral-latest/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>,
-<?php download_link("ProofGeneral-latest/doc/PG-adapting.ps.gz", "ps") ?> 
-or  
-<?php download_link("ProofGeneral-latest/doc/PG-adapting.pdf", "pdf") ?>.
-</p>
-
-
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<h2><a name="prerel">Pre-release: ProofGeneral-3.5pre040207</a></h2>
-
-<p> 
-Check the 
-<!-- WARNING!  Line below automatically edited by makefile. --> 
-<?php fileshow("ProofGeneral-3.5pre040207/CHANGES","CHANGES"); ?> file 
-<!-- End Warning. --> 
-for a summary of changes since the last stable
-version, and notes about work-in-progress.  </p> 
-<table width="80%" cellspacing=8> 
-<tr><td width=150>gzip'ed tar file</td>
-<!-- WARNING!  Lines below automatically edited by makefile. -->
-<td><?php download_link("ProofGeneral-3.5pre040207.tar.gz") ?></td>
-</tr>
-<tr>
-<td>zip file</td>
-<td><?php download_link("ProofGeneral-3.5pre040207.zip") ?></td>
-</tr>
-<tr>
-<td>RPM package </td>
-<td><?php download_link("ProofGeneral-3.5pre040207-1.noarch.rpm") ?></td>
-</tr>
-<tr>
-<td>individual files</td>
-<td><a href="ProofGeneral">http access to files in development release</a>
-</tr>
-</table>
-<!-- End Warning. -->
-<p> 
-<b>Emacs versions:</b>
-This version has been tested with XEmacs version 21.4.12 and with GNU
-Emacs 21.2.1.  XEmacs support is better tested, although use under
-GNU Emacs has certain advantages (e.g., nested comments!).  Please check
-<?php fileshow("ProofGeneral-3.5pre040207/CHANGES","CHANGES"); ?> 
-for detailed notes.  Older releases of Emacs
-<i>may</i> work, but we recommend the use of these or newer versions
-because backwards compatibility across different Emacs versions is far
-too difficult to support.  If you cannot upgrade your Emacs, consider
-using an <a href="oldrel.php">older release</a> of Proof General.
-</p> 
-<p>
-<b>Prover versions:</b>
-This version has been tested with Coq 7.4, Isabelle2003, Lego 1.3.1,
-and PhoX 0.8.
-</p>
-<b>Bundled packages:</b>
-Proof General is now bundled with several Emacs packages, to
-save the effort needed of installing them separately, and to
-solve compatibility problems.  
-This <b>includes X-Symbol</b>, so you don't need to download
-it separately any more.  If you want to override PG's preference
-for it's own packages, simply load your versions into memory
-before starting Proof General (e.g. with <tt>(require 'x-symbol)</tt>
-in your <tt>.emacs</tt> file).
-<p>
-For install instructions, see 
-the <a href="download#install">stable version download</a>.
-</p>
-
-<p>
-</p>
-<p>
-</p>
-
-
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<h2><a name="devel">CVS snapshot of ProofGeneral-3.5pre040207 for developers</a></h2>
-<!-- End Warning. -->
-
-<ul>
-  <li> gzip'ed tar file: 
-<!-- WARNING!  Line below automatically edited by makefile. -->
-      <?php download_link("ProofGeneral-3.5pre040207-devel.tar.gz") ?>
-<!-- End Warning. -->
-  </li>
-</ul>
-<p>
-This tarball contains all of our development files, including some
-files not present in the released version of Proof General.
-Specifically:
-</p>
-<ul>
-  <li> the low-level developer's todo files 
-    (see <a href="devel#lowleveltodo">the developers page</a>)
-   and the detailed
-   <!-- WARNING!  Line below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.5pre040207/ChangeLog","ChangeLog"); ?>,
-   <!-- End Warning. -->
- </li>
-  <li> developer's Makefile used to generate documentation files 
-       and the release itself,</li>
-  <li> test files, image source files, the web pages, and sometimes </li>
-  <li> working instantiations of Proof General for new provers. </li>
-</ul>
-<p>
-Most people don't need this.  Note that there are no pre-built
-documentation files in the developer's release (developers can
-run Make, by definition).
-</p>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/doc b/html/doc
deleted file mode 100644
index a58717d8..00000000
--- a/html/doc
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/doc.html b/html/doc.html
deleted file mode 100644
index 466add09..00000000
--- a/html/doc.html
+++ /dev/null
@@ -1,140 +0,0 @@
-<h2>Manuals for Proof General</h2>
-
-<p>
-There is a short FAQ and two manuals for Proof General:
-</p>
-<ul>
-<li> the <a href="FAQ">FAQ</a>  (please send any contributions)
-<li> the <a href="userman">Proof General user manual</a>
-</li>
-<li> the <a href="adaptingman">Adapting Proof General manual</a>
-</li>
-</ul>
-<p>
-The second manual gives instructions on how to adapt Proof General to new 
-proof systems, it's not needed for ordinary use.
-For printing you can download:
-<ul>
-<li>
-<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "User manual [ps]") ?> and
-<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "Adapting manual [ps]") ?>, or
-</li>
-<li>
-<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "User manual [pdf]") ?>,
-<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "Adapting manual [pdf]") ?>
-</li>
-</ul>
-<p>
-The PostScript files are recommended over the PDF.
-Both manuals (HTML and Info formats) are included in the
-<a href="download">download</a>. When running Proof General the manual
-is available from the "Proof General" menu.  It should also appear in
-the system Info pages.
-If you're considering developing Proof General, please check
-that you are using the documentation for the most recent
-development version of Proof General, available with the
-<a href="develdownload">development download</a>.
-</p>
-
-<p>
-You can discuss Proof General with other users and receive
-announcements by joining our <a href="mailinglist.html">mailing
-list</a>.
-</p>
-
-
-<h2>Manuals for Emacs</h2>
-
-<p>If you're new to Emacs, it's recommended to try the Emacs tutorial,
-available inside Emacs by pressing <b>C-h t</b> (which means
-<tt>ctrl</tt>-with-<tt>h</tt> followed by <tt>t</tt>).  There are many
-other <b>C-h</b> commands, and the Help menu inside Emacs gives access
-to more help facilities.
-</p>
-<p>For on-line reading, these links might be helpful:
-<ul>
-<li>The <a href="http://www.gnu.org/manual/emacs/">Emacs user manual</a></li>
-<li>The <a href="http://www.gnu.org/manual/emacs-lisp-intro">
-  Emacs lisp introduction</a> and 
-  <a href="http://www.gnu.org/manual/elisp">Emacs lisp reference</a>.</li>
-</li>
-</ul>
-(You don't need to look at anything about lisp unless you're interested
-in developing Proof General).
-</p>
-<p>The corresponding manuals for XEmacs are
-available <a href="http://www.xemacs.org/Documentation/index.html">here</a> (xemacs.org).
-</p>
-
-
-
-
-
-
-<h2>References</h2>
-
-<p> Ideas for the future of Proof General are given here:
-</p>
-<ul>
-<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> and
-    <a href="http://http://www.informatik.uni-bremen.de/~cxl/">Christoph Lüth</a>
-    <b><i>Proof General meets IsaWin</i></b>.
-    Proc. User Interfaces for Theorem Provers 2003 (UITP'03) September 2003,
-    Rome, Italy.
-    Available as <?php download_link("papers/uitp03.pdf", "[pdf]") ?>.
-</li>
-
-<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-    <b><i>Protocols for Interactive e-Proof</i></b>.
-    Draft version, see 
-    <a href="http://homepages.inf.ed.ac.uk/da/drafts/#eproof">here</a>.
-</li>
-<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-    <b><i>Proof General Kit (white paper)</i></b>.
-    Draft version, see 
-    <a href="http://homepages.inf.ed.ac.uk/da/drafts/#white">here</a>.
-</li>
-</ul>
-<p> A technology overview of Proof General is given here:
-</p>
-<ul>
-<li> <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-    <a href="papers/pgoutline.ps.gz">Proof General: A Generic Tool for
-     Proof Development</a>.
-     <i>Tools and Algorithms for the Construction and 
-      Analysis of Systems, Proc TACAS 2000</i>, LNCS 1785.
-    <br>
-    Here are some <a href="papers/pgtalk.pdf">slides</a> 
-    used for this talk and some other presentations of Proof General.
-</li>
-</ul>
-<p> Proof General supports Script Management as documented in:
-</p>
-<ul>
-  <li> <a
-      href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
-      Bertot</a> and <a
-      href="http://www.inria.fr/croap/personnel/Laurent.Thery/me.html">Laurent
-      Th&eacute;ry</a>.  <a
-      href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A
-      generic approach to building user interfaces for theorem
-      provers</a>.  
-      <i>Journal of Symbolic Computation</i>, 25(7), pp. 161-194, February 1998.
-  </li>
- </ul>
- <p>
- It has support for Proof by Pointing, as documented in:
- </p>
- <ul>
-  <li> <a
-      href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
-      Bertot</a>, Thomas Kleymann-Schreiber and Dilip Sequeira.
-    <I>Implementing Proof by Pointing without a Structure Editor</I>.
-    LFCS Technical Report <a
-    href="http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>.
-    Also published as Rapport de recherche de l'INRIA
-    <a href="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia
-      Antipolis</a> <a
-      href="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a>
-  </li>
-</ul>
diff --git a/html/download b/html/download
deleted file mode 100644
index a58717d8..00000000
--- a/html/download
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/download.html b/html/download.html
deleted file mode 100644
index e34b5cbc..00000000
--- a/html/download.html
+++ /dev/null
@@ -1,248 +0,0 @@
-<h2>Please register</h2>
-<p>
-Before downloading Proof General, <i>please</i>
-<a href="register">register</a>.
-It's free, it only takes a moment.
-If you have already registered you do not need to do so again.
-<!-- Let's remove this rant for now.  
-The statistics collected from registrations are used to help
-make a case for support for Proof General, and nothing else.  
-It is likely that development of Proof General will <i>finish soon</i> 
-unless we 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 or even a paper letter to the <a
-href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>.  And if you
-can offer to help resource the development of Proof General
-in some way, please
-<a href="feedback">contact us</a>. -->
-</p>
-
-<p>
-You can join the
-Proof General
-<a href="mailinglist">mailing list</a>
-for announcements of new versions.
-Developers and early-adopters 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 and/or an
-old Emacs version, you may need to download one of the 
-<a href="oldrel.php">previous releases</a>.
-</p>
-<h2><a name="stable">
-    Proof General Version 3.4, released 29th August 2002.
-    </a>
-</h2>
-<p>
-Proof General is distributed under the terms of
-the 
-<?php fileshow("ProofGeneral/COPYING","GNU General Public License"); ?>.
-<br>
-See <a href="#prereq">below</a> for software pre-requisites for running Proof General.
-</p>
-
-<p>
-Proof General is available as an archive and an RPM package.
-</p>
-<table width="80%" cellspacing=8>
-<tr>
-<td width=150>gzip'ed tar file</td>
-<td><?php download_link("ProofGeneral-3.4.tar.gz") ?></td>
-</tr>
-<tr>
-<td>zip file</td>
-<td><?php download_link("ProofGeneral-3.4.zip") ?></td>
-</tr>
-<tr>
-<td>RPM package </td>
-<td><?php download_link("ProofGeneral-3.4-1.noarch.rpm") ?>
-<br>NB: to build yourself use the tar file with <tt>rpm -ta</tt>.</td>
-</tr>
-<tr>
-<td>individual files</td>
-<td><a href="ProofGeneral-3.4">browse individual files</a>
-</tr>
-</table>
-<p>
-The archives and RPM include almost everything: the generic 
-code, specific code for the supported provers, installation 
-instructions and documentation in Info and HTML formats.
-Documentation is available in other formats
-here <a href="doc">here</a>.  
-<!-- 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.4 and
-GNU Emacs 21.2.  It should work with <i>some</i> earlier versions of
-XEmacs, but we recommend using these Emacs versions for the most
-reliable results.  Support on GNU Emacs is catching up, but XEmacs is
-still the better tested and more fully-featured environment.
-See below for links.
-</p>
-<p>
-See the <?php
-fileshow("ProofGeneral-3.4/etc/announce","announcement"); ?> for more
-details, or check the <?php
-fileshow("ProofGeneral-3.4/CHANGES","CHANGES"); ?> file for a summary
-of changes since version 3.3.
-</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," ); ?>)
-before reporting problems.  If you find a problem not already mentioned, 
-please 
-<?php hlink("feedback.html","send us a note","Feedback form")?>.
-</p>
-
-<br>
-
-<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 21.4 
-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 21.2 of 
-<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
-<br>
-Both Emacsen are available for a variety of platforms, including
-Unix variants, Windows 95/98/NT/2k, and Mac OS.
-</li>
-<li>
-A proof assistant, for example:
-<?php fileshow("ProofGeneral/coq/README","Coq"); ?>;
-<?php fileshow("ProofGeneral/isa/README","Isabelle"); ?>
-&nbsp;or <?php fileshow("ProofGeneral/isa/README","Isabelle/Isar"); ?>;
-<?php fileshow("ProofGeneral/lego/README","LEGO"); ?>;
-<?php fileshow("ProofGeneral/phox/README","PhoX"); ?>.
-<br>
-(click on links for version details; see <a href=".">front page</a> for
-other assistants).
-<br>
-Or write your own support for a new assistant!
-</li>
-</ul>
-</p>
-
-<p>
-There is also an <strong>optional</strong> component for using
-Proof General:
-<ul>
-<li>
-For displaying logical and mathematical symbols, the excellent
-<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
-package. 
-<br>It's very easy to install.  See <a href="#xsyminstall">here</a> 
-for installation notes.
-<br>Versions of X-Symbol supported:
-<b>version 3.4 (stable)</b>, and <i>partially</i>, <b>version 4.4 (beta)</b>.
-<br>
-The stable version of X-Symbol only works with XEmacs on systems running X.
-The beta version also works with Emacs 21.4 (not yet available), and 
-has limited support for XEmacs on Windows.
-</li>
-<!-- <li> -->
-<!-- For GNU Emacs, a version of <tt>func-menu.el</tt> to get  -->
-<!-- <a href="features#funcmenu">function menus</a>. -->
-<!-- <br>Unfortunately I can't find a version of this that -->
-<!-- works with current GNU 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>
-Compatibility across the multitude of Emacs versions is quite troublesome. 
-<br>
-XEmacs has been better tested with Proof General than GNU Emacs.
-<br>
-Earlier versions of either variant <i>may</i> work with Proof General
-but are not officially supported because we cannot test backward
-compatibility widely. Please <a href="feedback">send us fixes</a>
-rather than bug reports if you discover problems.
-Later versions of both Emacs variants <i>should</i> work with
-Proof General: if you discover problems, please check
-to see if they have been solved in a more recent
-<a href="develdownload">development release</a> before
-reporting.
-
-
-<h3><a name="install">Easy installation of Proof General</a></h3> 
-<p>
-To use Proof General, simply unpack the sources with 
-</p>
- <blockquote>
-   <tt>tar xpzf ProofGeneral-3.4.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.4/INSTALL","INSTALL")?> 
-file in the distribution for more details.
-</p>
-
-<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> 
-
-<p>
-X-Symbol is easy to install in XEmacs 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/xemacs-packages<br>
- cd ~/.xemacs/xemacs-packages<br>
- tar xpzf ../x-symbol-pkg.tar.gz<br>
-</tt></blockquote>
-<p>
-For GNU Emacs, you must remove the <tt>.elc</tt> files supplied, and
-add some code to your <tt>.emacs</tt>.  See 
-<a href="http://x-symbol.sourceforge.net/news.html">this page</a>
-for details.
-More installation options are given
-in the <a href="http://x-symbol.sourceforge.net/man/x-symbol_2.html">the X-Symbol manual</a>.
diff --git a/html/eeproof b/html/eeproof
deleted file mode 100644
index 2df23c96..00000000
--- a/html/eeproof
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('eeproof.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/eeproof.php b/html/eeproof.php
deleted file mode 100644
index 445fead7..00000000
--- a/html/eeproof.php
+++ /dev/null
@@ -1,32 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Engineering Electronic Proof"); 
-  ?>
-
-<p>
-The <b>Engineering Electronic Proof</b> project is 
-a proposed continuation of the Proof General project,
-using Proof General as a vehicle to study and build
-new mechanisms for managing the development of
-electronic proof.
-</p>
-
-<h3>Details</h3>
-<p>
-More details will be posted here in due course.
-</p>
-<p>
-In the meantime, there is some related
-information on the <a href="kit">Proof General Kit</a>
-page about the next stages of development for Proof General.
-</p>
-<p>
-<h3>Collaborations</h3>
-Collaborations on this work are being sought.  If you are interested in collaborating, or have ideas or suggestions to contribute, please send a note to
-<a href="mailto:da+pg-eeproof@inf.ed.ac.uk"><tt>da+pg-eeproof@inf.ed.ac.uk</tt></a>
-</p>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/elispmarkup.php3 b/html/elispmarkup.php3
deleted file mode 100644
index e2b47367..00000000
--- a/html/elispmarkup.php3
+++ /dev/null
@@ -1,137 +0,0 @@
-<?php
-//
-// Markup Emacs Lisp and Outline files
-//
-// David Aspinall, March 2000
-//
-// $Id$
-//
-//
-
-function isexpanded($headingno,$expanded) {
-  //  print "testing $headingno";
-  $all = ereg("all",$expanded);
-  $thisone = ereg("," . $headingno,$expanded);
-  return ($all ? ! $thisone : $thisone);
-}
-
-function addexpanded($headingno,$expanded) {
-  $all = ereg("all",$expanded);
-  return ($all ? str_replace("," . $headingno,"",$expanded) :
-	         $expanded . "," . $headingno);
-}
-
-function removeexpanded($headingno,$expanded) {
-  $all = ereg("all",$expanded);
-  return ($all ? $expanded . "," . $headingno : 
-		 str_replace("," . $headingno,"",$expanded));
-}
-
-function link_toggle($headingno,$text,$thispage,$filename,$expanded) {
-    if (isexpanded($headingno,$expanded)) {
-      $newexpanded=removeexpanded($headingno,$expanded);
-    } else {
-      $newexpanded=addexpanded($headingno,$expanded);
-    }
-  print "<a name=\"$headingno\"><a href=\"$thispage";
-  print "?file=" . urlencode($filename);
-  print "&expanded=" . urlencode($newexpanded) . "#" . $headingno . "\">" . $text . "</a></a>\n";
-}
-
-// FIXME: this is a nonsense really.  Might be okay if it
-// used dynamic HTML but it's too much of a faff at the moment.
-// Also, we should use the tree structure properly and keep a stack!
-
-function outline_markup($filename,$thispage,$expanded)  {
-  if ($title=="") { $title=$filename; };
-  $outline = false;
-  $file = file($filename);
-  $i = 0;
-  $level=0;
-  $headingno=0;
-  /* Now parse file, watching for outline headers */
-  for (;$i < count($file);$i++)  {
-     $line = $file[$i];
-     // HTML escapes
-     $line = htmlentities($line);
-     // Anchors for URLs
-     $line = ereg_replace("((http://|mailto:)[^ \n\t]+)","<a href=\"\\1\">\\1</a>",$line);
-     // Assume a heading
-     $multipar=false;
-     if (ereg("-\*- (mode:)?outline -\*-",$line)) {
-       // Found line with outline mode header, set flag
-       // and print message
-       $outline = true;
-       print "<p><i>";
-       print "This is a flattened outline file: click on a title to hide/reveal the leaf underneath it.";
-       print "<br>Click "; 
-       print "<a href=\"$thispage?file=" . urlencode($filename);
-       print "&expanded=all\">here</a> to show whole body, or ";
-       print "<a href=\"$thispage?file=" . urlencode($filename);
-       print "\">here</a> to hide whole body.";
-       print "</i></p>\n";
-     } elseif ($outline) {
-       if (ereg("^ *\n",$line)) {
-	 // if (!newpara) { print "</p><p>\n"; };
-	 $newpara = true;
-       } elseif (ereg("^([\*]+) (.*)\n",$line,$heading)) {
-	 $newlevel = strlen($heading[1])+1;
-	 //	 if ($newlevel < $level) {
-	 // Up a level
-	 //  $p = strpos($path,"-");
-	 //  $path = substr($path,0,$p-1);
-	 if ($newpara && 
-	     $level<=$newlevel && 
-	     isexpanded($headingno,$expanded)) { print "<p>\n"; }
-	 $headingno++;
-	 $level=$newlevel;
-	 $text="<h$level>$heading[2]</h$level>";
-	 link_toggle($headingno,$text,$thispage,$filename,$expanded);
-       } elseif (isexpanded($headingno,$expanded)) {
-	 if ($newpara && $level==0) { print "<p>\n"; }
-	 print $line;
-	 $newpara=false;
-	 $level=0;
-       }
-     } else {
-       print $line;
-     }
-  }
-}
-
-//
-// For browsing source.  Unfinished.
-//
-
-function elisp_markup($filename,$thispage,$title="")  {
-  if ($title=="") { $title=$filename; };
-  $file = file($filename);
-  $i = 0;
-  $level=0;
-  $headingno=0;
-  /* Now parse file, watching for outline headers */
-  for (;$i < count($file);$i++)  {
-     $line = $file[$i];
-     // HTML escapes
-     $line = htmlentities($line);
-     // Pagebreaks
-     // ??? 
-     // Anchors for URLs
-     $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","<a href=\"\\1\">\\1</a>",$line);
-     // Font-lock equivalents...
-     // 1. comments.  Strings roughly done: ignore if quote appears after ;
-// seems buggy: <div> breaks line in pre formatting.  Only do for whole-lines.
-//     $line = ereg_replace("^([^;]*)(;+[^\"^\n]+)\n$",
-     $line = ereg_replace("^(;+[^\"^\n]+)\n$",
-		          "<font color=\"#8080E0\">\\1</font>\n",
-			  $line);
-     // 2. keywords
-     $line = ereg_replace("^\(def(macro|un|var|custom|const|group|face)",
-			  "(<font color=\"#F0B0B0\">def\\1</font>",
-			  $line);
-     // FIXME: add hrefs for keywords, looking up in TAGS file.
-     // FIXME: add line numbers
-     // FIXME: parse strings
-     print $line;
-  }
-}
diff --git a/html/eproofe b/html/eproofe
deleted file mode 100644
index 4965773a..00000000
--- a/html/eproofe
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('eeproof.php'); ?>
-<?php
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links
-     in cvs. */ ?>
diff --git a/html/eproofe.php b/html/eproofe.php
deleted file mode 100644
index e965a78a..00000000
--- a/html/eproofe.php
+++ /dev/null
@@ -1,30 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Engineering Electronic Proof"); 
-  ?>
-
-<p> 
-Proof General, and particularly, the <a href="kit">Proof General
-Kit</a> is proposed as a vehicle for research into <i>engineering
-electronic proof<i>.  We want to investigate the
-maintenance, combination, and reuse of formal proof developments.
-</p>
-
-<h3>Planning</h3>
-<p>
-This project has not yet been started, and there are no public
-documents available yet.
-</p>
-<p>
-Some hints of our plans appear in the papers describing
-the <a href="kit">Proof General Kit</a>.
-</p>
-
-<p>
-Any <a href="mailto:da@dcs.ed.ac.uk">comments</a> are welcomed.
-</p>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/favicon.ico b/html/favicon.ico
deleted file mode 100644
index d3faa231..00000000
--- a/html/favicon.ico
+++ /dev/null
diff --git a/html/features b/html/features
deleted file mode 100644
index a58717d8..00000000
--- a/html/features
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/features.html b/html/features.html
deleted file mode 100644
index ebe5bb27..00000000
--- a/html/features.html
+++ /dev/null
@@ -1,210 +0,0 @@
-<!-- FIXME: would be nice to provide links from features
-  mentioned here to user-manual. -->
-<h2>Features of Proof General</h2>
-<p>
-It doesn't matter if you're an Emacs militant or a pacifist!
-</p>
-
-<p> The aim of Proof General is to provide powerful and configurable
-interfaces which help user-interaction with proof assistants.  Proof
-General targets power users rather than novices, but is designed to be
-useful to both.  Proof General leads to an environment for serious
-<i>proof engineering</i> of interactively-constructed proofs.
-</p>
-<p>Proof General is used by many people for organizing large proof
-developments, and also for teaching interactive proof. 
-They enjoy the following features:</p>
-</p>
-<dl>
-  <?php dt("Script management","script") ?>
-  <dd>
-  A <em>proof script</em> is a sequence of commands sent to
-  a proof assistant to construct a proof, usually stored in
-  a file.  <em>Script management</em> connects the editing of a 
-  proof script directly to an interactive proof process,
-  maintaining consistency between the edit buffer
-  and the state of the proof assistant.
-  <p>
-  Proof General colours a proof script to show the state in the proof
-  assistant.  Parts of a proof script that have been processed are
-  displayed in blue and are "locked" -- they cannot be edited.  Parts
-  of the script currently being processed by the proof assistant are
-  shown in red.  Bodies of completed proofs in the locked region
-  can be hidden from view to help browsing.  
-  Proof General has commands for processing new parts
-  of the buffer, or undoing already processed parts.  
-  </p>
-  <p>
-  Take a look at these
-  <a href="screenshot">screenshots</a>
-  of Proof General to see script management in action.
-  </p>
-  </dd>
-</dl><dl>
-  <?php dt("Simplified interaction model","simple") ?>
-  <dd>
-  Proof General is designed for proof assistants which have a
-  command-line (shell) interpreter.  When using Proof General, the proof
-  assistant's shell is hidden from the user.  Communication takes
-  place via three buffers (Emacs text widgets).  The <i>script
-  buffer</i> holds input, the commands to construct a proof.  The
-  <i>goals buffer</i> displays the current list of subgoals to be
-  solved.  The <i>response buffer</i> displays other output from the
-  proof assistant.  By default, only two of these three buffers are
-  displayed at once.  This means that the user only sees the output
-  from the most recent interaction, rather than a screen full of
-  output from the proof assistant.
-  <p>
-  Despite this more friendly communication model, Proof General does not
-  commandeer the proof assistant shell: the user still has complete
-  access to it if necessary.
-  </p>
-  </dd>
-</dl><dl>
-  <?php dt("Multiple files","multiple") ?>
-  <dd>
-  Script management in Proof General can work across many script
-  files, integrating with the file handling of
-  the proof assistant.  When a script is visited in the editor, it 
-  is locked (coloured) to reflect whether the proof assistant has 
-  loaded it in this session.  When a file is unlocked, all of the 
-  files which depend on it are automatically unlocked too.
-  <p> 
-  Dependencies between script files are either communicated from the
-  proof assistant to Proof General, or maintained automatically by
-  Proof General (based on the order in which files were processed).
-  </p>
-  </dd>
-</dl><dl>
-  <?php dt("Subterm highlighting and proof by pointing","pbp") ?>
-  <dd>
-  <p>
-  Using hidden markup in the concrete syntax, Proof General allows the
-  user to explore the structure of complex terms output by the prover.
-  This provides nifty features for cutting-and-pasting subterms,
-  querying the type of a subterm, looking up the definition of an
-  identifier, and so on.
-  </p>
-  <p>
-  <em>Proof by pointing</em> uses this markup to allow the prover
-  to suggest steps in a proof, guided by the user's gestures
-  in displayed goals.  For example, clicking on a hypothesis inserts 
-  a proof step into the script to solve a goal using that hypothesis, 
-  and executes it.
-  </p>
-  <?php footnote("Subterm markup is only fully supported by LEGO at the moment, with an experimental implementation of proof by pointing.  Isabelle highlights only variables.  If you would like to see these features better supported in your favourite proof assistant, please canvas the implementor to add subterm-markup support.")  ?>
-  </dd>
-</dl><dl>
-  <?php dt("Toolbar and menus","toolbar") ?>
-  <dd>
-  Proof General has a toolbar with buttons for examining
-  the proof state, starting a proof, manoeuvring in the proof script, 
-  restarting the prover, saving a proof, searching for a theorem,
-  issuing a command, interrupting the assistant, and getting help.
-  <p>
-  Using the toolbar, you can replay proofs without knowing any 
-  low-level commands of the proof assistant or any Emacs hot-keys! 
-  <p>
-  Additionally, the toolbar commands and many more besides are
-  available on menus; you don't need to know magical key presses for
-  any features.
-  </p>
-  </dd>
-</dl><dl>
-  <?php dt("Syntax highlighting","fontlock") ?>
-  <dd>
-  Syntax highlighting is an editing feature which decorates a file
-  with different colours or fonts according to the syntax of some
-  language (usually a programming language). 
-  <p>
-  Proof General decorates proof scripts: proof commands are
-  highlighted and different fonts may be used for definitions and
-  assumptions, for example.
-  </p>
-  </dd>
-</dl><dl>
-  <?php dt("Real symbols","xsymbol") ?>
-  <dd>
-  Proof General has a close integration with the
-  powerful 
-  <a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
-  package, which makes it easy to transparently use real symbols and
-  Greek letters in your proofs.  
-  <br> 
-  Instead of seeing "not P", you see "&not; P", instead
-   of "a * b", you see "a &times; b", etc. 
-  <br>
-   (Those examples are simple so they will work on most browsers 
-    without needing images, see the
-    <a href="screenshot">screenshots</a> for more examples.)
-  <p>
-  </dd>
-</dl><dl>
-  <?php dt("Proof-script editing facilities","funcmenu") ?>
-  <dd>
-  <p>
-  Many facilities are provided for editing proof scripts.   
-  The <i>completion</i> mechanism of Emacs can be used to
-  help type keywords and identifier names.
-  The <i>outline</i> mode of Emacs allows hiding of parts of proof scripts;
-  a further special <i>proof hiding</i> facility is provided to
-  hide the body of completed proofs.
-  <i>Navigation</i> in the script is supported by a pull-down menu 
-  which gives easy access to the theorems, definitions, and declarations
-  in the current buffer.  
-  </p>
-<!-- it is in FSF Emacs if you download func-menu.el from somewhere -->
-<!--   <?php footnote("Definitions menu is available in XEmacs only") ?> -->
-  <p>
-  </dd>
-</dl><dl>
-  <?php dt("Remote proof assistant.") ?>
-  <dd>
-  Sometimes you may want to run a proof assistant on a powerful remote
-  machine.  Proof General can communicate with a proof assistant running
-  remotely, while your files and editor reside on your local machine.
-  <p></p>
-  </dd>
-</dl><dl>
-  <?php dt("Tags","tags") ?>
-  <dd>
-  Tags are an editing feature which allow you to quickly locate the
-  definition or declaration of a particular identifier.  Proof General
-  is supplied with utilities to make tag indexes for Emacs.
-  This makes it easy to quickly access
-  definitions from a standard library, for example, and in large proof
-  developments split across multiple files.
-<!--   <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
-  <p></p>
-  </dd>
-</dl><dl>
-  <?php dt("Adaptability","generic") ?>
-  <dd>
-  Proof General is designed to be adaptable.  Many aspects
-  of its behaviour can be easily customized (using dialogue boxes and
-  buttons, no text file editing!).   
-  <p>
-  Most importantly, Proof General is generic, so you can adapt it to 
-  a new proof assistant with surprisingly little effort.
-  <p>
-  Adapting for a new proof assistant is mainly a matter of setting
-  some variables with regular expressions to help parse output from
-  the prover, and setting other variables with commands to send to the
-  prover.  See this basic
- <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", 
-	  "example instance"); ?>.
-  To get the most from Proof General (proof by pointing, for
-  example), it may be necessary to put some hooks in
-  the output routines of the proof assistant.  
-  </p>
-  Please feel free to download Proof General to customize it for a new
-  system, and 
-  <?php hlink("feedback.html","tell us ","Feedback form")?>
-  how you get on.
-  </dd>
-</dl>
-<p>
-For (even) more details of Proof General's features, see the manuals and
-papers on the <a href="doc">documentation page</a>.
-</p>
-
diff --git a/html/feedback b/html/feedback
deleted file mode 100644
index 94066bcf..00000000
--- a/html/feedback
+++ /dev/null
@@ -1,6 +0,0 @@
-<?php include('feedback.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
-
diff --git a/html/feedback.php b/html/feedback.php
deleted file mode 100644
index e599bfcd..00000000
--- a/html/feedback.php
+++ /dev/null
@@ -1,89 +0,0 @@
-<?php
-##
-##  Proof General feedback form.
-##  
-##  David Aspinall, June 1999.
-##
-##  $Id$
-##
-  require('functions.php3');
-
-  if ($argv[0] !="submit"): 
-###
-### Feedback form
-###
-  small_header("Proof General Feedback Form"); 
-?>
-
-<p>
-Please use the form below to send us comments, suggestions,
-or offers to help with Proof General development.
-Or simply send an email directly to
-the <?php mlinktxt($project_feedback, "Proof General maintainer &lt;$project_feedback&gt."); ?>
-</p>
-<p>
-You can also report a bug using this form, although it would
-be more helpful to do this from within Emacs, using the 
-"<kbd>Proof General -> Submit bug report</kbd>" menu command.
-</p>
-
-<form method=post action="<?php print $PHP_SELF . "?submit"; ?>">
-<table width="450" border="0" cellspacing="2" cellpadding="0">
-<tr>
-  <td width="20%">From:</td>
-  <td width="80%"><input type=text name="from" size="40"></td>
-</tr>
-<tr>
-  <td>Subject:</td>
-  <td><input type=text name="subject" size="40"></td>
-</tr>
-<tr><td colspan="2">
-<textarea rows="15" cols="70" wrap="physical" name="feedback">
-Dear Proof General developers,
-</textarea>
-(For us to reply, please include a proper email
- address in the From box).
-</td></tr>
-<tr><td></td><td>
-<p align=right>
-<input type=reset value="Clear">
-<input type=submit value="Send feedback"> 
-</p>
-</td></tr>
-</table>
-</form>
-
-<?php  
-   click_to_go_back(); 
-   footer(); 
-  else:
-##
-##  Process feedback
-##
-   small_header("Thank-you!"); 
-   
-   /* NB: No validation of address! */
-
-   /* FIXME: could append extra info to feedback. */
-
-   $message = "From:\t\t" . $from . "\nSubject:\t" . $subject 
-	   . "\n\n" . "Message:\n" . $feedback;
-
-   if ($from != "") { print "<p>Dear " . $from . ",</p>\n"; };
-   print "<p>";
-   print "Thank-you for sending us feedback";
-   if ($subject != "") { print " about " . $subject; };
-   print ".</p>\n<p>";
-   print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read.";
-   print "</p>";
-
-   mail($project_feedback,  
-	"[Web Feedback Form]: " . $subject,
-	$message,
-        "Reply-To: " . $from . "\n");
-
-   click_to_go_back();
-  
-   footer();
-endif;
-?>
diff --git a/html/fileshow.php b/html/fileshow.php
deleted file mode 100644
index ded131d6..00000000
--- a/html/fileshow.php
+++ /dev/null
@@ -1,8 +0,0 @@
-<?php
-  require('functions.php3');
-  require('elispmarkup.php3');
-  $filename=$HTTP_GET_VARS["file"];
-  $title=$HTTP_GET_VARS["title"];
-  $expanded=$HTTP_GET_VARS["expanded"];
-  fileshowmarkup($file,$title,$expanded);
-?>
diff --git a/html/footer.html b/html/footer.html
deleted file mode 100644
index 77709857..00000000
--- a/html/footer.html
+++ /dev/null
@@ -1,10 +0,0 @@
-<!-- This is the footer -->
-<hr>
-<address>
-Web pages by
-<a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-<br>
-Contact
-<?php mlinktxt($project_feedback, "Proof General maintainer."); ?>
-<br>
-
diff --git a/html/functions.php3 b/html/functions.php3
deleted file mode 100644
index 78610cc3..00000000
--- a/html/functions.php3
+++ /dev/null
@@ -1,337 +0,0 @@
-<?php
-//
-// Dave's PHP Header
-//
-// Included in every page.  
-// Prints DTD, <html> opening tag,
-// and defines some useful functions.
-//
-// David Aspinall, June 1999/2002.
-//
-// $Id$
-//
-//
-
-
-// Project configuration
-
-$project_email = "da+pg-feedback@inf.ed.ac.uk";
-$project_list  = "da+pg-users@inf.ed.ac.uk";
-$project_feedback = "da+pg-feedback@inf.ed.ac.uk";
-
-// Disable when free parking forwarding is broken
-// $proofgenatdcs = "proofgen@dcs.ed.ac.uk";
-// $project_email = $proofgenatdcs;
-// $project_list  = $proofgenatdcs;
-// $project_feedback = $proofgenatdcs;
-
-$project_title = "Proof General";
-
-$project_subtitle = "Organize your Proofs!";
-$project_full_title = $project_title . " --- " . $project_subtitle;
-
-if ($title == "") { $title = $project_title; }  // default page title.
-
-///////////////////////////////////////////////////////////////////
-//
-// DTD 
-//
-
-$dtd_strict = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.0//EN\" \"http://www.w3.org/TR/REC-html40/strict.dtd\">\n";
-$dtd_loose = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.0 Transitional//EN\" \"http://www.w3.org/TR/REC-html40/loose.dtd\">\n";
-$xml_header="<?xml version=\"1.0\"?>";
-$dtd_xml_loose ="<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">";
-$dtd_xml_strict ="<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">";
-$html="<html>\n";
-$xhtml="<html xmlns=\"http://www.w3.org/1999/xhtml\">\n";
-
-print $dtd_loose;
-print $html;
-
-//print $xml_header;
-//print $dtd_xml_strict;
-//print $xhtml;
-
-
-// Validator address
-
-// $validator = "http://validator.dcs.ed.ac.uk/";
-// It's a private link which won't work elsewhere, but never mind.
- $validator = "http://localhost/validator/";
-
-function mlink($addr) {
-  print "<a href=\"mailto:" . $addr . "\">" . $addr . "</a>";
-}
-
-function mlinktxt($addr,$txt) {
-  print "<a href=\"mailto:" . $addr . "\">" . $txt . "</a>";
-}
-
-
-// FIXME: doesn't seem to work.  Why not?
-function project_email() {
-  mlink($project_email);
-}
-
-
-/* Style sheet element for dt doesnt work in Netscape 4, so hack it here.  
-   NB!  This violates HTML 4 DTD.
-*/
-function dt($string,$name="") {
-  print "<dt>";
-  if ($name != "") { print "<a name =\"$name\">"; }
-  print "<div style=\"font-style:italic; font-weight: bold\">";
-  print $string;
-  print "</div>";
-  if ($name != "") { print "</a>"; }
-  print "</dt>";
-}
-
-/* Automatic footnotes? */
-/* FIXME: for now, just inline them. */
-
-function footnote ($text) {
-   print "<p><i><small>[" . $text . "]</small></i></p>";
-}
-
-/* A hyper-link with optional mouse over text.
-   Could be made more sophisticated to do roll-overs, 
-   or whatever.
-*/
-
-function hlink ($url,$text,$mouseover="") {
-  print "<a href=\"" . $url . "\"";
-  if ($mouseover != "") {
-	print " onMouseOver=\"window.status='" . $mouseover . "'; return true;\"";
-  };
-  print ">" . $text . "</a>";
-}
-
-/* Determining download sizes (print broken message if file not found) */
-
-function download_size($filename) {
-   if (file_exists($filename)) {
-	$size = filesize($filename);
-        $sizek = (int) ($size/1024);
-   	print " (";
-   	if ($sizek == 0) {
-	     print $size . " bytes)";
-   	} else {
-	     print $sizek . "k)";
-   	}
-   } else {
-	print " (link broken)";
-   }
-}
-
-function download_link($filename,$linkname = "") {
-   print "<a href=\"" . $filename . "\">";
-   if ($linkname == "") { 
-	print $filename;
-   } else {
-	print $linkname;
-   };
-   print "</a>";
-   print download_size($filename);
-}
-
-function date_modified($filename) {
-   $time = filemtime($filename);
-   if ($time) {
-	print "Last modified " . strftime("%d %B %Y",$time) . ".\n";
-   }
-}
-
-function small_header($title) {
-  include('head.html');
-  include('smallheader.html'); 
-  print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
-}
-
-function small_header_body($title) {
-  include('smallheader.html'); 
-  print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
-/*  print "<p>";  FIXME: hack to get CSS to work with bad HTML from texi2html */
-}
-
-/* FIXME: remove this function: maybe just set a global variable,
-   or use SCRIPT_NAME, and then include footer.html. */
-
-function footer($filemodified=".") {
-  global $project_feedback;
-  include('footer.html'); 
-  date_modified($filemodified);
-  print "</address>\n";
-//  print "</font>\n";  /* Naughty stuff for older browsers, shouldn't do if V4 */
-  print "</body>\n";
-  print "</html>\n";
-}
-
-function click_to_go_back() {
-  // FIXME: the empty href no longer refers to the root,
-  // so this use of "/" breaks relative linking.
-  print "<p>\nClick <a href=\"/\">here</a> to go back to the ";
-  print $project_title; // FIXME: doesn't work, prints nothing.
-  print " front page.</p>\n";
-}
-
-/* Link to a marked up file */
-/* NB: could determine type automatically! */
-
-function fileshow($filename,$text="",$title="") {
- if ( $text == "") { $text=$filename; };
- $message=$title;
- if ( $message == "") { $message=$filename; };
- $titlecode = ($title == "" ?  "" : "&title=" . urlencode($title));
- hlink("fileshow.php?file=" . urlencode($filename) . $titlecode,
-	$text, $message);
-}
-
-function fileshowmarkup($filename,$title="",$expanded="") {
-  if ($title=="") { $title = $filename; };
-  small_header($title);
-  print "<pre>\n";
-  /* I hope this is enough to prevent access outside cwd */
-  if (substr($filename,0,1)=="." or 
-      substr($filename,0,1)=="/" or
-      substr($filename,0,1)=="~") {
-     print "Sorry, can't show you that file!\n"; 
-  } elseif (substr($filename,-3)==".el") {
-     elisp_markup($filename,"fileshow.php");
-  } else {
-     outline_markup($filename,"fileshow.php",$expanded);
-  }
-  print "</pre>\n";
-  print "<hr>";
-  click_to_go_back();
-  footer();
-}
-
-/* Similar for html file (NB: could pick automatically) */
-
-function htmlshow($filename,$text="",$title="") {
- if ( $text == "") { $text=$filename; };
- $message=$title;
- if ( $message == "") { $message=$filename; };
- $urlbits = parse_url($filename);
- hlink("htmlshow.php"
-       . "?title=" . urlencode($title) 
-       . "&file=" . urlencode($urlbits["path"])
-       . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
-	$text, $message);
-}
-
-function htmlshow_link($filename,$title="") {
- $urlbits = parse_url($filename);
- return "htmlshow.php"
-   . "?title=" . urlencode($title) 
-   . "&file=" . urlencode($urlbits["path"])
-   . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]);
-}
-
-
-/* Markup plain text file, by escaping < and > */
-
-function markup_plain_text($filename) {
-  $file = file($filename);
-  for($i = 0;$i < count($file);$i++) {
-     $line = $file[$i];
-     $line = ereg_replace("<","&lt;",$line);
-     $line = ereg_replace(">","&gt;",$line);
-     print $line;
-  };
-}
-
-/* Hack an html file to be shown with our style sheet
-   and hack relative links to go via htmlshow.php. 
-   This isn't particularly robust, but seems to work for
-   the output of texi2html.
-*/
-
-function hack_html($filename,$title="",$docrooturl="")  {
-  if ($title=="") { $title=$filename; };
-  if ($docrooturl=="") {
-     $docrooturl = "htmlshow.php?title=" . urlencode($title);
-  }
-  $file = file($filename);
-  /* Paste style sheet in head */
-  for($i = 0;$i < count($file);$i++) {
-     $line = $file[$i];
-     if (eregi("</HEAD>",$line)) {
-        /* Paste in style sheet */
-	print "<style type=\"text/css\">\n<!--";
-	include("proofgen.css");
-	print "-->\n</style>\n";
-        /* End style sheet paste in */
-        print $line;
-	$i++;
-	break;
-     } else { print $line; };
-  }
-  /* Now parse rest of document, hacking relative links. */
-  /* Matching here is not great, will get confused by html tags inside strings, etc. */
-  for (;$i < count($file);$i++)  {
-     $line = $file[$i];
-       /* PHP has no way to get the match position, so we have to 
-	  match a suffix of the line, add extra parenthesis, and calculate it. */
-     while (eregi("(<A([^>]*)(HREF=\"([^\"]+)\")(.*))",$line,$linebits)) { 
-       /* found URL in a particularly simple form */
-       $matchpos = strlen($line) - strlen($linebits[1]);
-       print substr($line,0,$matchpos);		/* start of line */
-       $line = $linebits[5];			/* rest of line after link */
-       $urlbits = parse_url($linebits[4]);
-       if ($urlbits["host"]=="") { 
-	  /* Assume a relative link, let's hack it. */
-	  if ($urlbits["path"]=="") {
-	     /* A fragment in same file */
-	     $newurl = $docrooturl . "#" . $urlbits["fragment"];
-	  } else {
-	     /* Another file, use same title */
-	     /* FIXME: would be nice to deal with split info files
-		here by adding aliases somehow */
-	     $newurl = "htmlshow.php?title=" . urlencode($title) 
-                . "&file=" 
-	    	. urlencode(dirname($filename) . "/" . $urlbits["path"])
-		. ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]);
-	  };
-	  print "<A " . $linebits[2] . " HREF=\"" . $newurl . "\"";
-	} else { print "<A " . $linebits[2] . $linebits[3]; }
-     };
-     /* Hack on a header and footer */
-     if (eregi("<BODY.*>",$line)) { 
-       /* Assume there's nothing else interesting on the line, whoops. */
-       print $line;
-       small_header_body($title);
-     } elseif (eregi("</BODY>",$line)) {
-       /* Assume there's nothing else interesting on the line, whoops. */
-       click_to_go_back();
-       print $line;
-     } else {
-       print $line;
-     };
-  }
-}
-
-
-
-/* Display a small page with standard header, footer added on.
-   Much like htmlshow.  */
-
-function smallpage($filename,$text="",$title="",$message="") {
- if ( $text == "") { $text=$filename; };
- if ( $message == "") { $message=$title; };
- if ( $message == "") { $message=$filename; };
- $urlbits = parse_url($filename);
- hlink("smallpage.php"
-       . "?title=" . urlencode($title) 
-       . "&file=" . urlencode($urlbits["path"])
-       . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
-	$text, $message);
-}
-
-/* Specialised version for projects */
-
-function pgproject($filename,$title) {
-   smallpage("projects/$filename.html",$title,"Proof General Project",$title);
-}
-
diff --git a/html/gallery b/html/gallery
deleted file mode 100644
index 7342616d..00000000
--- a/html/gallery
+++ /dev/null
@@ -1,6 +0,0 @@
-<?php include('gallery.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
-
diff --git a/html/gallery.php b/html/gallery.php
deleted file mode 100644
index 977b4797..00000000
--- a/html/gallery.php
+++ /dev/null
@@ -1,84 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Gallery"); 
-  ?>
-
-<blockquote>
-<p>
-Here are some publicity pictures for Proof General.  They were created
-by David Aspinall in his spare time, using the excellent freeware
-programs <a href="http://www.gimp.org">GIMP</a> and <a
-href="http://www.blender.org">Blender</a>.  The General himself is
-based on a commercial mesh given away by 
-<a href="http://www.viewpoint.com">Viewpoint</a>.
-</p>
-<p>
-Click on a thumbnail to see a full-size images.  All full-size images
-are 720x990 pixel JPGs (a nice size to print at 180dpi on A5 paper).
-Please download and print for your own use!  
-<p>
-Copyright for the images is held by 
-<a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
-Please do not publish the images or incorporate them into other
-work without his permission.  If you have comments or suggestions,
-or if you would like a copy of one of the images
-in another size or format, 
-please <a href="feedback">contact us</a>.
-</p>
-
-</p>
-<p>
-For pictures of what Proof General looks like in use,
-see the <a href="screenshot">screenshots</a> page.
-</p>
-</blockquote>
-
-<!-- todo: php3 this -->
-<table width="80%">
-<tr>
-<td width="200">
-<a href="images/portrait.jpg">
-<img src="images/portrait-thumb.jpg" alt="Portrait" width=150 height=206 border=0>
-</a>
-</td>
-<td>
-<p>
-Proof General portrait <br>
-This is the Proof General logo, 
-with the home page URL at the bottom. <br>
-A nice poster for your wall or door. <br>
-</p>
-</tr>
-<tr>
-<td>
-<a href="images/whip.jpg">
-<img src="images/whip-thumb.jpg" alt="New recruit" width=150 height=206 border=0>
-</a>
-</td>
-<td>
-<p>
-New Recruits Wanted  <br>
-This is a request for help with the Proof General
-project. <br>
-Please <a href="feedback">sign up here</a>!
-</p>
-</tr>
-<tr>
-<td>
-<a href="images/whole-man.jpg">
-<img src="images/whole-man-thumb.jpg" alt="Whole man" width=150 height=206 border=0>
-</a>
-</td>
-<td>
-<p>
-Scary boots!  <br>
-This is a full-length shot of Proof General,
-again with the home page at the bottom.
-</p>
-</tr>
-</table>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/head.html b/html/head.html
deleted file mode 100644
index cdd344b8..00000000
--- a/html/head.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<head>
-    <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-    <meta name="author" content="David Aspinall <da@dcs.ed.ac.uk>">
-    <meta name="keywords" content="Isabelle, LEGO, Coq, Emacs, XEmacs, 
-      Interface, Theorem Prover, GUI, David Aspinall">
-    <meta name="description" content="Proof General is an Emacs based 
-      generic interface for theorem provers">
-    <link rel="stylesheet" href="proofgen.css" type="text/css">
-    <link rel="SHORTCUT ICON" href="favicon.ico">
-    <title><?php print $title ?></title>
-</head>
- <!-- Duplicate some style entries in body elt to support Version 3 browsers. 
-      FIXME: Shouldn't really serve this mess up to V4s and later. -->
-<!-- <font face="Verdana, Arial, LucidaSans, sans-serif;">-->
-<body
- bgcolor="#2D1D03"
- background="images/canvaswallpaper.jpg"
- text="#FFFFFF"
- link="#FFD820"
- vlink="#FFD820"
- alink="#FFF030"
- >
diff --git a/html/header.html b/html/header.html
deleted file mode 100644
index b335ac24..00000000
--- a/html/header.html
+++ /dev/null
@@ -1,61 +0,0 @@
-<!-- This is the header -->
-<table width="650">
-<tr>
-<td width="100">
-<a href=".">
-<img src="images/ProofGeneral.jpg" alt="Proof General" width=90 height=119 border=0>
-</a>
-</td>
-<td>
-<center>
-  <img src="images/pg-text.gif" alt="Proof General" width=170 height=17 border=0>
-  <h1>Organize your proofs!</h1>
-<?php
-      /* Header link generator.  David Aspinall, June 1999.
-       * Based orginially on navbar.php3 by Douglas Campbell
-       * Look for $WANTED in array.  If not found, use default of "Home"
-       * and fix $WANTED.  Hrefs are given by page parameter to current doc.
-       */
-    $separator='<td width=10em><img align=left src="images/bullethole.gif" width=15 height=15 alt=".">&nbsp;';
-    $urlbits = parse_url($REQUEST_URI);
-    $file = ereg_replace("^(.*/)+","",$urlbits["path"]);
-    $WANTED = ereg_replace(".html","",$file);
-    print "<table  width=\"80%\" class=\"menubar\"><tr align=\"left\">\n"; 
-    $links_arr  =  array(
-          "Home"          =>  "main", 
-	  "Features"	  =>  "features",
-	  "Download"      =>  "download",
-          "Documentation" =>  "doc",
-
-          "News"          =>  "news", 
-          "Screenshots"   =>  "screenshot",
-	  "Development"	  =>  "devel",
-	  "About"	  =>  "about"
-    );
-    $DEFAULT = $links_arr["Home"];
-    $wanted_okay = 0;
-    for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
-	  if ($WANTED  ==  $links_arr[$name]) {
-		$wanted_okay = 1;
-	  }
-    };
-    if (! $wanted_okay) {
-	$WANTED = "main";
-    };
-    for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
-        print  $separator;
-        if  ($WANTED  ==  $links_arr[$name])  {
-	  print "<font color=\"white\">" . $name . "</font>";
-	  }
-	else {
-          print "<a href=\"$links_arr[$name]\">$name</a>";
-	}
-        print " </td>\n";
-        if ($name=="Documentation") print "</tr >\n<tr>";
-    }
-    print "</tr></table>\n"; 
-?>
-</td></tr>
-</table>
-</center>
-<!-- End of header -->
\ No newline at end of file
diff --git a/html/hits b/html/hits
deleted file mode 100644
index 6d5c2be6..00000000
--- a/html/hits
+++ /dev/null
@@ -1,26 +0,0 @@
-<?php
-  $counterFile = "counter.txt";
-  $counterStart = "counterstart.txt";
-  $maxlen=10;
-  require('functions.php3');
-  small_header("Hit counter");
-  print "<p>";
-  if (is_readable($counterFile)) {
-     print "These pages have been accessed ";
-     readfile($counterFile);
-     print " times ";
-     if (is_readable($counterStart)) {
-     	$fp=fopen($counterStart,"r");
-     	$start=fgets($fp,20);
-	print "since ";
-     	print strftime("%d %B %Y",$start);
-     	print ".\n";
-     } else {
-        print "<br>\n(could not access time stamp file $counterStart)\n";
-     };
-  } else {
-     echo "Could not access hit counter file $counterFile\n";
-  };
-  print "</p>";
-  footer();
-?>
diff --git a/html/htmlshow.html b/html/htmlshow.html
deleted file mode 100644
index d9cb8b46..00000000
--- a/html/htmlshow.html
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php
-  require('functions.php3');
-  hack_html($file,$title);
-  footer(); 
-?>
diff --git a/html/htmlshow.php b/html/htmlshow.php
deleted file mode 100644
index 915aac6f..00000000
--- a/html/htmlshow.php
+++ /dev/null
@@ -1,11 +0,0 @@
-<?php
-  require('functions.php3');
-  if (substr($file,0,1)=="." or 
-      substr($file,0,1)=="/" or
-      substr($file,0,1)=="~") {
-     print "Sorry, can't show you that file!\n"; 
-  } else {
-     hack_html($file,$title);
-  }
-  footer(); 
-?>
diff --git a/html/images/.cvsignore b/html/images/.cvsignore
deleted file mode 100644
index 5c165d91..00000000
--- a/html/images/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-.xvpics
diff --git a/html/images/IsaPGscreen.jpg b/html/images/IsaPGscreen.jpg
deleted file mode 100644
index 5e2dda74..00000000
--- a/html/images/IsaPGscreen.jpg
+++ /dev/null
diff --git a/html/images/PG-small.jpg b/html/images/PG-small.jpg
deleted file mode 100644
index 50bb9cf6..00000000
--- a/html/images/PG-small.jpg
+++ /dev/null
diff --git a/html/images/ProofGeneral.jpg b/html/images/ProofGeneral.jpg
deleted file mode 100644
index d2c430cd..00000000
--- a/html/images/ProofGeneral.jpg
+++ /dev/null
diff --git a/html/images/bullethole.gif b/html/images/bullethole.gif
deleted file mode 100644
index 1eb03072..00000000
--- a/html/images/bullethole.gif
+++ /dev/null
diff --git a/html/images/canvaswallpaper.jpg b/html/images/canvaswallpaper.jpg
deleted file mode 100644
index 8062bd4e..00000000
--- a/html/images/canvaswallpaper.jpg
+++ /dev/null
diff --git a/html/images/coq-badge.gif b/html/images/coq-badge.gif
deleted file mode 100644
index 901e7645..00000000
--- a/html/images/coq-badge.gif
+++ /dev/null
diff --git a/html/images/coqlogo4.gif b/html/images/coqlogo4.gif
deleted file mode 100644
index 5899de81..00000000
--- a/html/images/coqlogo4.gif
+++ /dev/null
diff --git a/html/images/coqlogo4.xcf b/html/images/coqlogo4.xcf
deleted file mode 100644
index 21cd46cb..00000000
--- a/html/images/coqlogo4.xcf
+++ /dev/null
diff --git a/html/images/isabelle-badge.gif b/html/images/isabelle-badge.gif
deleted file mode 100644
index 8da95453..00000000
--- a/html/images/isabelle-badge.gif
+++ /dev/null
diff --git a/html/images/isabelle.gif b/html/images/isabelle.gif
deleted file mode 100644
index 171b2101..00000000
--- a/html/images/isabelle.gif
+++ /dev/null
diff --git a/html/images/lego-badge.gif b/html/images/lego-badge.gif
deleted file mode 100644
index 182ad85f..00000000
--- a/html/images/lego-badge.gif
+++ /dev/null
diff --git a/html/images/pg-coq-screenshot.png b/html/images/pg-coq-screenshot.png
deleted file mode 100644
index eb071514..00000000
--- a/html/images/pg-coq-screenshot.png
+++ /dev/null
diff --git a/html/images/pg-coq-thumb.png b/html/images/pg-coq-thumb.png
deleted file mode 100644
index 1510b502..00000000
--- a/html/images/pg-coq-thumb.png
+++ /dev/null
diff --git a/html/images/pg-isa-screenshot.png b/html/images/pg-isa-screenshot.png
deleted file mode 100644
index e903e4e3..00000000
--- a/html/images/pg-isa-screenshot.png
+++ /dev/null
diff --git a/html/images/pg-isa-thumb.png b/html/images/pg-isa-thumb.png
deleted file mode 100644
index d0db67cc..00000000
--- a/html/images/pg-isa-thumb.png
+++ /dev/null
diff --git a/html/images/pg-isar-screenshot.png b/html/images/pg-isar-screenshot.png
deleted file mode 100644
index 6ea369de..00000000
--- a/html/images/pg-isar-screenshot.png
+++ /dev/null
diff --git a/html/images/pg-isar-thumb.png b/html/images/pg-isar-thumb.png
deleted file mode 100644
index bc558d56..00000000
--- a/html/images/pg-isar-thumb.png
+++ /dev/null
diff --git a/html/images/pg-lego-console-thumb.png b/html/images/pg-lego-console-thumb.png
deleted file mode 100644
index 0a44450a..00000000
--- a/html/images/pg-lego-console-thumb.png
+++ /dev/null
diff --git a/html/images/pg-lego-console.png b/html/images/pg-lego-console.png
deleted file mode 100644
index 0e7c22a3..00000000
--- a/html/images/pg-lego-console.png
+++ /dev/null
diff --git a/html/images/pg-lego-screenshot.png b/html/images/pg-lego-screenshot.png
deleted file mode 100644
index e8c6b749..00000000
--- a/html/images/pg-lego-screenshot.png
+++ /dev/null
diff --git a/html/images/pg-lego-thumb.png b/html/images/pg-lego-thumb.png
deleted file mode 100644
index 6f650baa..00000000
--- a/html/images/pg-lego-thumb.png
+++ /dev/null
diff --git a/html/images/pg-text.gif b/html/images/pg-text.gif
deleted file mode 100644
index cf592478..00000000
--- a/html/images/pg-text.gif
+++ /dev/null
diff --git a/html/images/phox-einstein.jpg b/html/images/phox-einstein.jpg
deleted file mode 100644
index 97af4ee3..00000000
--- a/html/images/phox-einstein.jpg
+++ /dev/null
diff --git a/html/images/portrait-thumb.jpg b/html/images/portrait-thumb.jpg
deleted file mode 100644
index d84d27b4..00000000
--- a/html/images/portrait-thumb.jpg
+++ /dev/null
diff --git a/html/images/portrait.jpg b/html/images/portrait.jpg
deleted file mode 100644
index a23f0f16..00000000
--- a/html/images/portrait.jpg
+++ /dev/null
diff --git a/html/images/silverrule.gif b/html/images/silverrule.gif
deleted file mode 100644
index 3ad7fbda..00000000
--- a/html/images/silverrule.gif
+++ /dev/null
diff --git a/html/images/vh40.gif b/html/images/vh40.gif
deleted file mode 100644
index c5e9402e..00000000
--- a/html/images/vh40.gif
+++ /dev/null
diff --git a/html/images/whip-thumb.jpg b/html/images/whip-thumb.jpg
deleted file mode 100644
index 16aac5b4..00000000
--- a/html/images/whip-thumb.jpg
+++ /dev/null
diff --git a/html/images/whip.jpg b/html/images/whip.jpg
deleted file mode 100644
index 1a6341b6..00000000
--- a/html/images/whip.jpg
+++ /dev/null
diff --git a/html/images/whole-man-thumb.jpg b/html/images/whole-man-thumb.jpg
deleted file mode 100644
index 32175a27..00000000
--- a/html/images/whole-man-thumb.jpg
+++ /dev/null
diff --git a/html/images/whole-man.jpg b/html/images/whole-man.jpg
deleted file mode 100644
index f3fff341..00000000
--- a/html/images/whole-man.jpg
+++ /dev/null
diff --git a/html/index.php b/html/index.php
deleted file mode 100644
index 3eb50db3..00000000
--- a/html/index.php
+++ /dev/null
@@ -1,8 +0,0 @@
-<?php require('functions.php3'); ?>
-<?php  include('head.html'); ?>
-<?php
-    include('header.html');
-    include($WANTED . '.html' . $WANTEDFRAG);
-    footer();
-?>
-
diff --git a/html/index.shtml b/html/index.shtml
deleted file mode 100644
index d4bdff95..00000000
--- a/html/index.shtml
+++ /dev/null
@@ -1,3 +0,0 @@
-<!-- This is the entry point to the Proof General web pages -->
-<!--#include file="counter.php3"-->
-<!--#include file="index.php"-->
diff --git a/html/kit b/html/kit
deleted file mode 100644
index d7ba8cb2..00000000
--- a/html/kit
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('kit.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/kit.html b/html/kit.html
deleted file mode 100644
index d7ba8cb2..00000000
--- a/html/kit.html
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('kit.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
diff --git a/html/kit.php b/html/kit.php
deleted file mode 100644
index 9785f01c..00000000
--- a/html/kit.php
+++ /dev/null
@@ -1,74 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Kit"); 
-  ?>
-
-<p>
-The Proof General Kit project is in an early experimental stage at
-the moment.  If you are interested in collaborating, or have ideas
-or suggestions to contribute, please send a note to
-<a href="mailto:da+pg-kit@inf.ed.ac.uk"><tt>da+pg-kit@inf.ed.ac.uk</tt></a>
-</p>
-
-<h3>Planning</h3>
-<p>
-Ideas for the future of Proof General are described in these papers:
-</p>
-<ul>
-<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-    <b><i>Protocols for Interactive e-Proof</i></b>.
-    Draft version, see 
-    <a href="http://homepages.inf.ed.ac.uk/da/papers/drafts/#eproof">here</a>.
-</li>
-<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.
-    <b><i>Proof General Kit (white paper)</i></b>.
-    Draft version, see 
-    <a href="http://homepages.inf.ed.ac.uk/da/papers/drafts/#white">here</a>.
-</li>
-</ul>
-
-<h3>Development</h3>
-<p>
-Work which is currently in progress includes:
-<ul>
- <li>The definition of PGIP and PGML, as 
-     <a href="http://www.relaxng.org">RELAX NG</a> schemas.<br>
-     Recent versions: 
-      <?php download_link("Kit/dtd/pgip.rnc") ?>,
-      <?php download_link("Kit/dtd/pgml.rnc") ?>.
-     <br/>
-     The derived DTDs are:
-      <?php download_link("Kit/dtd/pgip.dtd") ?>,
-      <?php download_link("Kit/dtd/pgml.dtd") ?>.
-     <br/>
-     There is also a <b>draft</b> commentary available,
-      <?php download_link("Kit/docs/commentary.pdf") ?>.
-     <br/>
-     This updates the white paper mentioned above.
-
- </li>
- <li>Together with <a href="http://www.informatik.uni-bremen.de/~cxl/">Christoph Lüth</a>:
-     a Haskell front-end and PGIP mediator, described in a
-       <a href="http://www.informatik.uni-bremen.de/uitp03/">UITP '03</a>
-       paper <a href="Kit/docs/uitp03.pdf">here</a>.
- <li>With assistance from Isabelle developers at Munich:
-     a PGIP-enabled version of Isabelle/Isar
-     (patch available soon).
- </li>
- <li>Work on <b>Eclipse Proof General</b>, an 
-	<a href="http://www.eclipse.org">Eclipse</a> front end for Proof General
-     (new project sponsored by IBM 
-	<a href="http://www-306.ibm.com/software/info/university/products/eclipse/eig.html">
-	award</a>).
- </li>
-</ul>
-</p>
-<p>
-We hope to make an alpha version of some software available in the
-not-<em>too</em>-distant future. 
-</p>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/links b/html/links
deleted file mode 100644
index a58717d8..00000000
--- a/html/links
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/links.html b/html/links.html
deleted file mode 100644
index f18d20f0..00000000
--- a/html/links.html
+++ /dev/null
@@ -1,71 +0,0 @@
-<h2>Related projects</h2>
-<p>
-Here are some links to related things.  
-If you have any suggestions 
-for links to include here, please
-<?php hlink("feedback","contact us","Feedback form")?>.
-</p>
-
-<ul>
-<li><a href="http://homepages.inf.ed.ac.uk/da/Isamode">Isamode</a>
-  is an XEmacs front-end for Isabelle.  It has a different
-  feature collection compared with Proof General:
-  script management is not supported, but there are extensive
-  menus and shortcuts provided for common Isabelle
-  commands.
-</li>
-</ul>
-<ul>
-<li><a href="http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html">CtCoq</a>
-  is an interface for the Coq theorem prover, developed
-  at INRIA, Sophia Antipolis, as part of
-  <a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
-  Like Proof General, CtCoq is based on a general approach for
-  building user-interfaces for theorem provers, although no other
-  current theorem provers are supported.  Unlike Proof General, CtCoq
-  is based on a graphical environment with structure editing,
-  created with the <a
-  href="http://www-sop.inria.fr/croap/centaur/centaur.html">Centaur</a>
-  system.
-</li>
-</ul>
-<ul>
-<li>
-  <a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a> is
-  a collection of web-based distributed tools for supporting
-  theorem proving.
-</li>
-</ul>
-<ul>
-<li>
-  <a href="http://www.dcs.gla.ac.uk/prosper/">Prosper</a> is a project
-  to develop an extensible, open proof tool architecture for
-  incorporating formal verification into industrial CAD/CASE tool
-  flows and design methodologies. The tools include novel
-  user-friendly interfaces.
-</li>
-</ul>
-<ul>
-<li>
-  As a possible foundation for generic proof environments,
-  <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>
-  is a standard representation form for mathematical objects, which
-  links in with the <a href="http://www.w3.org/Math/">MathML</a>
-  markup language.
-</li>
-</ul>
-<ul>
-<li>
-  <a href="http://www.mrg.dist.unige.it/omrs/index.html">Open Mechanized Reasoning System (OMRS)</a>
-</li>
-</ul>
-<ul>
-<li>
-  <a href="http://www.cs.unibo.it/~asperti/HELM/home.html">Hypertextual Electronic Library of Mathematics (HELM)</a>
-</li>
-</ul>
-<ul>
-<li>
-  The <a href="http://eti.cs.uni-dortmund.de/eti/servlet/ETISiteApplication">Electronic Tool Integration</a> Platform.
-</li>
-</ul>
diff --git a/html/mailinglist b/html/mailinglist
deleted file mode 100644
index d957589e..00000000
--- a/html/mailinglist
+++ /dev/null
@@ -1,66 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Mailing Lists"); 
-  ?>
-
-<p>
-The Proof General Users mailing list is a low-volume list
-used for announcements of new versions, and occasional
-discussions amongst users.
-</p>
-<p>
-This list is <i>not</i> for those having problems with the
-software: please contact 
-<a href="mailto:da+pg-support@inf.ed.ac.uk">da+pg-support@inf.ed.ac.uk</a>
-in the first instance.
-</p>
-
-<h3>Subscriptions</h3>
-<p>
-To <b>subscribe or unsubscribe</b>, visit
-the 
-<a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral">Mailman
-web page</a> for the list.
-<br>
-Alternatively, you can send a message to 
-<a href="mailto:proofgeneral-request@informatics.ed.ac.uk">
-<tt>proofgeneral-request@informatics.ed.ac.uk</tt></a>
-with the word "<tt>subscribe</tt>" (or "<tt>unsubscribe <it>password</it></tt>")
-in the message body.
-</p>
-
-
-<h3>Posting</h3>
-<p>
-The canonical mailing list address is 
-<a href="mailto:da+pg-users@inf.ed.ac.uk"><tt>da+pg-users@inf.ed.ac.uk</tt></a>.
-<br>
-This is an alias for
-<tt>proofgeneral@informatics.ed.ac.uk</tt>.
-</p>
-<p>
-In an effort to prevent spam, posting is restricted to list members.
-Please <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral">subscribe here</a> before attempting to post.
-</p>
-
-<h3>Archives</h3>
-<p>
-Archives of the list (since July 2002) are kept
-<a href="http://lists.informatics.ed.ac.uk/pipermail/proofgeneral">here</a>.
-</p>
-
-<h3>Proof General Developers list</h3>
-<p>
-There is a separate mailing list for those interested in the
-development of Proof General.  The canonical address
-for this list is <a href="mailto:da+pg-devel@inf.ed.ac.uk"><tt>da+pg-devel@inf.ed.ac.uk</tt></a>.
-Again, posting is restricted to list members.
-Please visit the <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral-devel">Mailman web page</a> for subscription details.
-</p>
-
-
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/mailinglist.html b/html/mailinglist.html
deleted file mode 100644
index 59a74d27..00000000
--- a/html/mailinglist.html
+++ /dev/null
@@ -1,6 +0,0 @@
-<?php include('mailinglist'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
-
diff --git a/html/main b/html/main
deleted file mode 100644
index a58717d8..00000000
--- a/html/main
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/main.html b/html/main.html
deleted file mode 100644
index fdffc920..00000000
--- a/html/main.html
+++ /dev/null
@@ -1,145 +0,0 @@
-<h2>What is Proof General?</h2>
-<p>
-<b>Proof General</b> is a generic interface for proof assistants, 
-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>.
-</p>
-<p>
-To find out more, check the
-<a href="features"> features list</a>
-and look at the
-<a href="screenshot">screenshots</a>.
-To get Proof General, visit the
-<a href="download">download page</a>.
-If you're not interested in interactive proof,
-see the <a href="components">standalone components</a>
-developed as part of Proof General.
-To contact the developers, click
-<?php hlink("feedback","here","Feedback form")?>.
-</p>
-
-
-
-<h2>What systems does Proof General work with?</h2>
-
-<p>Proof General comes ready-to-go for these proof
-assistants:</p>
-
-<table width="90%">
- <tr>
-   <td align="center">
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-      "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
-      "The Isabelle Home Page"); ?>
-   </td>
-   <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-		    "Isabelle", "The Isabelle Home Page"); ?>
-      <br>
-       <div style="font-size: smaller">
-       By 
-      <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>
-       and
-       Markus Wenzel.
-       </div>
-   </td>
- </tr>
-  <tr>
-    <td align="center">
-       <?php hlink("http://pauillac.inria.fr/coq/",
-		   "<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?>
-      </td>
-    <td>
-     <b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for 
-       <?php hlink("http://pauillac.inria.fr/coq/",
-		   "Coq","The Coq Home Page") ?>
-       <br>
-	<div style="font-size: smaller">
-         By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
-	 <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
-        </div>
-    </td>
- </tr>
- <tr>
-    <td align="center">
-       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
-       "<img src=\"images/phox-einstein.jpg\" width=80 height=48 border=0 alt=\"PhoX logo\">",
-       "The PhoX Home Page") ?>
-   </td>
-    <td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for
-       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
-		   "PhoX","The PhoX Home Page") ?>
-       <br>
-       <div style="font-size: smaller">
-       By 
-       <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
-       and
-       <a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>.
-       </div>
-    </td>
- </tr>
- <tr>
-    <td align="center">
-       <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
-       "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
-       "The LEGO Home Page") ?>
-   </td>
-    <td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for
-       <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
-		   "LEGO","The LEGO Home Page") ?>
-       <br>
-       <div style="font-size: smaller">
-       By Thomas Kleymann, Dilip Sequeira, 
-       <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>
-       and
-       <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
-       </div>
-    </td>
- </tr>
-</table>
-
-<p>There are also <i>experimental</i> or <i>in-development</i> instances
-of Proof General:</p>
-
-<ul>
-<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof
-General"); ?></b>, for <a
-href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.</li>
-
-<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof
-General"); ?></b>, for <a
-href="http://www.twelf.org">Twelf</a>.</li>
-
-<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof
-General"); ?></b>, for <a
-href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.</li>
-
-<li><b><?php fileshow("ProofGeneral/plastic/README","Plastic Proof
-General"); ?></b>, for <a
-href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a> 
-(in development).</li>
-
-
-<li><b><?php fileshow("ProofGeneral/lclam/README","Lambda-Clam Proof
-General"); ?></b>, for <a href="http://dream.dai.ed.ac.uk/software/lambda-clam/">Lambda-CLAM</a>
-(in development).</li>
-</ul>
-
-<p>The instances of Proof General marked "in development" above are
-not considered complete, but are supported by the developers of proof
-systems.  The other instances above are "technology demonstrations" of
-Proof General for other popular provers, but only show a bare fraction
-of what is possible. We are seeking volunteers to support and improve
-each of these (please <a href="feedback">send a note to <tt><?php
-print $project_feedback; ?></tt></a> if you're interested).</p>
-
-<p>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
-configuration</a> is provided.</p>
diff --git a/html/mission.html b/html/mission.html
deleted file mode 100644
index a0203092..00000000
--- a/html/mission.html
+++ /dev/null
@@ -1,136 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Mission (draft)"); 
-  ?>
-
-<center>
-<h2>Mission Statement</h2>
-<h2>Proof General Developers</h2>
-<h2>March 2000</h2>
-</center>
-
-<p>
-We seek to provide an interface suite for helping users interact with
-<a href="#pas"><i>proof assistants</i></a>.
-</p>
-
-<p>
-Our approach is based on these principles:
-<ul>
-<li>
-Be useful to both <a href="#experts"><i>experts and novices</i></a>.
-</li>
-<li>
-Be <a href="scalable"><i>scalable</i></a> to large proof developments.
-</li>
-<li>
-Be <a href="#learn"><i>easy to learn</i></a>, 
-yet still provide advanced features.
-</li>
-<li>
-Be <a href="#generic"><i>generic</i></a> 
-to support many proof assistants with
-a uniform interaction mechanism.
-</li>
-<li>
-Be a <a href="#quality"><i>high-quality</i></a> research prototype.
-</li>
-</ul>
-</p>
-<p>
-Above all, we take a <i>pragmatic</i> approach to constructing
-interfaces.  Our primary aim is to provide a tool which is
-immediately useful for proof engineering.
-</p>
-<p>
-This aim means that we harness a range of 
-<a href="#proven">proven techniques</a>
-reimplemented in our generic system.
-Nevertheless, by the act of constructing Proof General, we do invent
-and incorporate some <a href="#novel">novel advances</a> which
-contribute to research in the field.
-</p>
-
-<hr>
-<p>
-</p>
-<h2>Footnotes and elaboration</h2>
-
-<dl>
-<?php dt("Proof assistants.","pas") ?>
-<dd>
-Computer programs for constructing formal machine proofs.  Terminology
-varies; we include all kinds of theorem proving systems
-which involve user interaction while a proof is constructed.  
-We currently focus on systems based on a notion of <i>proof
-script</i>, which is a file containing a user-level representation
-of the proof or how it was constructed.
-</dd>
-<?php dt("Experts and novices.","experts") ?>
-<dd>
-Many interfaces for proof assistants are aimed at novice or beginner
-users (and often used for teaching).  Instead, we want to provide an
-interface which is useful for expert users in the first place.
-But we believe such a system can also be helpful for beginner users.
-</dd>
-<?php dt("Scalability.","scalable") ?>
-<dd>
-Some interfaces fail to scale to large proof developments;
-we want Proof General to be useful for real-life, large
-projects, consisting of many theorems and theories.
-</dd>
-<?php dt("Easy to learn.","learn") ?>
-<dd>
-It is difficult enough to learn how to use the logic and language
-of a proof assistant, without an extra effort for learning its
-interface.  We want to provide a friendly interface with
-intuitive features, hence a shallow learning curve. 
-</dd>
-<?php dt("Genericity.","generic") ?>
-<dd>
-Proof General is intended to be used with a variety of underlying
-proof assistants.  We appreciate that different proof assistants are
-based on different logical principles, and implement different proof
-languages.  Yet interaction between different systems often has a
-similar behaviour.  We exploit this to provide a good user interface
-for many systems at once, saving repeated development effort by proof
-assistant implementors.  It has the added benefit of providing a
-uniform interaction mechanism between different systems, making it
-easier for users to experiment with several proof assistants.
-</dd>
-<?php dt("High-quality.","quality") ?>
-<dd>
-The developers are working on Proof General in the academic sector,
-and engineering work itself is not directly funded.  Despite this, we
-strive to follow good engineering practices to build a robust and
-maintainable system, which users can easily install (or test on the
-web).  To this end, we employ open-source development with frequent
-test releases before stable releases, and high-priority attention to
-user suggestions and bug reports.  We use CVS for source control,
-a strategy of bottom-up successive improvement, and provide support
-for each proof assistant by an experienced user/developer.
-</dd>
-<?php dt("Proven techniques.","proven") ?>
-<dd>
-Amongst other features, Proof General currently includes 
-<a href="features#script">script management</a>
-and
-<a href="features#pbp">proof-by-pointing</a>
-both championed in
-<a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
-</dd>
-<?php dt("Novel advances.","novel") ?>
-<dd>
-Proof General also advances the state-of-the-art.
-For example, we introduced proof-by-pointing in
-an free-form environment,
-and extended script management to handle
-<a href="features#multiple">multiple files</a>.
-</dd>
-</dl>
-
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/news b/html/news
deleted file mode 100644
index a58717d8..00000000
--- a/html/news
+++ /dev/null
@@ -1,5 +0,0 @@
-<?php include('index.php'); ?>
-<?php 
-  /* This file needs some extra characters in it for apache to work its magic.
-     Things work fine as link to index.html, but it's tricky to include links 
-     in cvs. */ ?>
\ No newline at end of file
diff --git a/html/news.html b/html/news.html
deleted file mode 100644
index f3e0068f..00000000
--- a/html/news.html
+++ /dev/null
@@ -1,60 +0,0 @@
-<h2>News about Proof General</h2>
-
-<ul>
-<li><b>11th December 2003</b>
-<p>
-Please <b>update your links!</b>.  The server <tt>zermelo.dcs.ed.ac.uk</tt>
-hosting Proof General for the last 5 years has now been retired.
-Moroever, the Proof General .org domain has been poached from us.
-</p>
-<p>
-Please refer to the web site using the URL
-<b><a href="http://proofgeneral.inf.ed.ac.uk">proofgeneral.inf.ed.ac.uk</a></b>
-and do not send any email to the old .org addresses (contact 
-David Aspinall directly).  Also, beware that the old addresses are built
-into the help function of Proof General and the bug reporting commands.
-Please download the upcoming pre-release (available soon) 
-which has offending addresses removed.
-</p>
-</li>
-
-<li><b>25th September 2003</b>
-<p>
-There is a new <a href="develdownload">development</a> version of
-Proof General released today.  There are some minor fixes, and an
-updated version of X-Symbol bundled.  Please test it and let me know
-how you get on.  It would be nice to release the final version 3.5 at
-last.
-</p>
-The <a href="kit">Proof General Kit</a> page has been
-updated to mention current development efforts.
-</p>
-<p>
-Anonymous access to the Proof General CVS repository is now available!
-Details are <a href="devel">here</a>.
-</p>
-</li>
-
-<li><b>29th August 2002</b>
-<p>
-<i>Proof General 3.4 is released.  Happy Proving!</i>
-<br>
-Go to the <a href="download">download page</a> to get it.
-<br>
-Please report any problems to <a href="mailto:da+pg-support@inf.ed.ac.uk"><tt>da+pg-support@inf.ed.ac.uk</tt></a>.
-</p>
-<li><b>1st July 2002</b>
-<p>
-Good news!  The license conditions for Proof General will shortly be
-changed to the <a href="http://www.gnu.org/copyleft/gpl.html">GPL</a>.
-This relaxes the current conditions in several ways, in particular,
-allowing packaging and distribution of the code by others.
-</p>
-</li>
-
-</ul>
-<!-- da: Put this line in instead if you're not me -->
-<!-- <i>(News items entered by <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> -->
-<!--     unless noted.)</i> -->
-<i>News items by <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.</i>
-<i>Click <a href="oldnews.html">here</a> for old news.</i>
diff --git a/html/notes.txt b/html/notes.txt
deleted file mode 100644
index 7d73ce30..00000000
--- a/html/notes.txt
+++ /dev/null
@@ -1,56 +0,0 @@
-Developers' Notes about Web Pages
----------------------------------
-
-NEW: server hacks needed to serve these pages, giving nice urls
-
- PHP3  module included
- .html treated as application
-
- Mime magic configured:
-
-LoadModule mime_magic_module  modules/mod_mime_magic.so
-AddModule mod_mime_magic.c
-MimeMagicFile /etc/httpd/conf/magic
-
-to recognize files beginning <?php, by
- adding this to /etc/httpd/conf/magic:
-
-0	string		<?php		application/x-httpd-php3
-
-Then add these links:
-
-  news -> index.html
-  doc -> index.html
-
-etc.
-
-***************
-
-Notes about php:
-
-Some functions I've written
-
- <?php hlink("html file","text","status message")?>
-
-NB: no space after text so you must write
- 
-   <?php ... ?> blah 
-
-to get a space.  Don't put "blah" onto a new line, space will
-be lost!
-
-
-*************
-
-Tell Thomas (& other folk?) to update his home page links to Proof General.
-[Probably okay: Thomas links to image in home directory, but we'll
- keep that as a copy of images/ProofGeneral.jpg]
-
-*************
-
-Suggestions for improving web pages after Rod reading them:
-
-  - slideshow rather than single screen shot
-  - separate feature list
-  - explain what a proof script is and what script management buys you
-
diff --git a/html/oldnews.html b/html/oldnews.html
deleted file mode 100644
index 47d7ebd7..00000000
--- a/html/oldnews.html
+++ /dev/null
@@ -1,411 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Old News"); 
-  ?>
-<ul>
-
-
-<li><b>19th June 2002</b>
-<p>
-We plan to release version <b>3.4</b> of Proof General 
-in August.  This update will have several significant 
-improvements
-(notably to the synchronization support for Coq), and also includes
-fixes and updates for recent versions of Emacs (notably GNU Emacs 21.x) 
-and various proof assistants.
-<br>
-<b>Please, please, please</b> do test some <a
-href="develdownload.html">development releases</a> for us in the
-meantime and <a href="feedback">report any difficulties</a>, 
-to help make the next release of Proof General as 
-robust as possible.  Thanks!
-</p>
-</li>
-
-<li><b>14th December 2001</b>
-<p>
-The current <a href="develdownload.html">development release</a> takes
-advantage of the new fancy features available in GNU Emacs 21, to add
-toolbar support and other features there.  As usual, maintaining the
-code to work with both Emacs versions is quite troublesome, so bug
-reports and patches from users are very welcome.
-</p>
-</li>
-
-<li><b>10th September 2001</b>
-<p>
-<a href="download">Proof General 3.3</a> is released, with
-<?php fileshow("ProofGeneral-3.3/CHANGES","new features"); ?> to
-increase your proof script editing efficiency.  Happy proving!
-</p>
-</li>
-<li><b>1st August 2001</b>
-<p>
-The past few months have seen a few more improvements and
-bug fixes to Proof General: many thanks to those who have
-sent us <a href="feedback">useful feedback</a>.
-It's time that we made a proper release, so please try
-out the <a href="develdownload.html">development release</a>
-and help us iron out as many more problems as we can.
-<br>
-Emacs Lisp and the Emacsen libraries has to be one of the
-worst moving target platforms to develop an application on,
-so please help us! Once things are looking good, we'll 
-release PG 3.3.
-</p>
-<li><b>8th May 2001</b>
-<p>
-Proof General has had a few quiet improvements since October, which
-appear in the current 
-<a href="develdownload.html">development release</a>.
-This version also has some compatibility fixes
-for the recent releases of Emacs (20.7) and XEmacs (21.4).
-</p>
-
-<li><b>2nd October 2000</b>
-<p>
-Proof General 3.2 is released today.  Happy proving!
-</p>
-
-<li><b>25th Sep 2000</b>
-<p>
-Final week of testing for Proof General 3.2.  
-The last chance to report bugs or request (minor) improvements for this release.
-Please help us by trying out the 
-<a href="develdownload.html">pre-release</a>, especially if you are
-relying on an older or non-standard Emacs version.
-Also check to see if the new 
-manuals are useful: now split into
-the user manual in
-<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>,
-<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "ps") ?> 
-or  
-<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "pdf") ?>,
-and the separate "adapting" manual, in
-<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>,
-<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "ps") ?> 
-or  
-<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "pdf") ?>.
-(Info files are included in the distribution).
-</p>
-<li><b>14th Sep 2000</b>
-<p>
-Improvements to web pages.  Graphics made smaller, text more concise.
-Please <?php hlink("feedback","send me suggestions ","Feedback form")?>
-for further improvements.
-(I know some pages display poorly in Netscape 4.7x because 
-of patchy stylesheet support; they appear much better in IE5
-or the rather impressive recent versions of KDE's Konqueror).
-</p>
-<li><b>28th Aug 2000</b>
-<p>
-We're starting the testing phase for Proof General 3.2.  
-It has several new features and improvements.
-Please try out the <a href="develdownload.html">pre-release</a>
-version, and report any problems to us.  Your
-feedback is very important because we have no resources available for
-serious compatibility testing ourselves.
-</p>
-<p>
-We hope to release 3.2 by the end of September.
-</p>
-</li>
-<li><b>25th May 2000</b>
-<p>
-Minor patch 3.1.6 released today.  This turns off toolbar enablers if
-you're running XEmacs on Solaris; because of strange Solaris problems,
-buttons are disabled too often there.  (You can live without
-this part of the patch by customizing the variable
-<tt>proof-toolbar-use-button-enablers</tt>). 
-The patch also removes 
-the use of an "interval timer" when 
-<tt>proof-toolbar-use-button-enablers</tt> is off, since a user 
-reported being unable to start itimers unless
-running as root (likely an operating system configuration problem).
-Thanks to Markus Wenzel and Pierre Lescanne for reporting problems.
-</p>
-</li>
-<li><b>5th May 2000</b>
-<p>
-New!  
-Proof General <?php fileshow("ProofGeneral/FAQ", "FAQ");?>.
-Please send questions or suggestions for inclusion to
-<a href="mailto:proofgen@dcs.ed.ac.uk">proofgen@dcs.ed.ac.uk</a>,
-thanks.
-</p>
-<li><b>28th April 2000</b>
-<p>
-A minor patch to Proof General 3.1 is released today.  To check what
-version you have, look at the variable <tt>proof-general-version</tt>
-set in <tt>proof-site.el</tt>.  (It is not recorded in the tar file
-name or package version).  The current patch, to 3.1.4, was made to
-fix a problem with Isabelle and theory file retraction, accidently
-introduced in 3.1.  See <?php
-fileshow("ProofGeneral-3.1-devel/etc/release-log.txt","the developer's
-release log"); ?> for details.
-NB: This patch was first made on 4th April, but didn't quite solve the
-problem.  Thanks to Mike Squire for sending a patch to fix the fix.
-</p>
-<p>
-Further improvements are being introduced in the new 3.2 pre-releases,
-see the 
-<a href="develdownload.html">development download</a> page, as usual.
-</p>
-<li><b>23rd March 2000</b>
-<p>
-Proof General 3.1 is now available from the
-<a href="download">download page</a>.  Enjoy!
-</p>
-</li>
-<li><b>14th March 2000</b>
-<p>
-Release candidate for Proof General 3.1 available.
-Pre-releases from now on are release candidates for version 3.1.
-Please test and report any problems you find
-(check the CHANGES and BUGS lists for issues known about
-and/or resolved).  Version 3.1 should be released next week.
-</p>
-</li>
-<li><b>10th March 2000</b>
-<p>
-New: <b>HOL Proof General</b>!
-It took me only a couple of hours to add a basic instantiation of
-ProofGeneral for 
-<a href="http://www.cl.cam.ac.uk/Researc/HVG/HOL/HOL.html">HOL98</a>.
-Most of this time was in trying to find out how to do things in HOL,
-I could have done with a HOL user to hand.  But I thought it was high time
-HOL got a look-in.
-</p>
-<p>
-HOL Proof General provides script management support, automatic
-multiple files, decoration of proof scripts and output.
-Character-sequence X Symbols as in Coq and LEGO.  Although this is a
-basic feature set for Proof General, the result is still an enormous
-improvement over shell interaction.
-</p>
-<p>
-My hope is to entice HOL users so that one of them may improve HOL
-Proof General.  I don't plan to maintain or seriously improve this
-instantiation myself.
-</p>
-<p>
-The HOL support is shipping in the 
-current <a href="develdownload.html">development release</a>.
-</p>
-</li>
-<li><b>15th February 2000</b>
-<p>
-There is now a new 
-<a href="devel">page for developers</a>.
-I plan to apply for funding to continue managing the evolution
-and development of Proof General, once my own job position
-is more secure.  
-Now is the time to flesh out ideas
-for the future!  
-Check the development page for the
-latest proposals.  These include some desirable contributions 
-which could be undertaken as self-contained projects.
-</p>
-<li><b>9th February 2000</b>
-<p>
-Countdown to Proof General 3.1 begins.  This will be a bug fix releaase.
-A few bugs have been fixed in
-recent Proof General development releases, one important one is fixing
-support for non-mule versions of GNU Emacs (thanks to Pierre Courtieu
-for raising it to my attention).  I would like to release PG 3.1 next
-month so that everyone can benefit.
-</p>
-<p>
-In the meantime, please 
-<?php 
-  hlink("feedback","report any important problems ","Feedback form")?>
-that you would like to see fixed, and consider trying out 
-the current <a href="devel">development release</a>.
-</p>
-<li><b>14th December 1999</b>
-<p>
-I'm pleased to say that Proof General will be demonstrated at
-<a href="http://iks.cs.tu-berlin.de/etaps2000/etaps.html">ETAPS 2000</a>.
-Here are some draft <a href="papers/pgtalk.pdf">slides</a> for 
-the presentation 
-(any <a href="mailto:David.Aspinall@ed.ac.uk">comments</a> would be welcome).
-A presentation of Proof General based on these slides was given at 
-<a href="http://www.clrc.ac.uk/">Rutherford Appleton Laboratory</a> last week.
-</p>
-<li><b>26th November 1999</b>
-<p>
-Proof General 3.0 is released!
-</p>
-<li><b>17th November 1999</b><br>
-<p>
-Proof General 3.0 is currently in final testing, and will be released
-in a small number of days.  Please help me with this by testing the
-current <a href="devel">pre-release</a>, so I can iron out as
-many bugs as possible before making the release.  It's very easy to
-install or upgrade Proof General, so it shouldn't be much effort to
-test it quickly.  Particularly if you're already running an earlier
-version.
-</p>
-<li><b>16th November 1999</b><br>
-<p>
-New!  With Proof General 3.0, adapting to a new prover is easier
-than ever before!
-It includes an 
- <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", "example instance ");?>
-of Proof General for Isabelle, which 
-configures the main core of the interface with less than 30 lines of
-code.  Not bad for getting about 4000 lines worth of code in benefit!
-</p>
-<li><b>9th November 1999</b><br>
-<p>
-Isabelle 99 was released last week, and Proof General 3.0 should
-be ready for release in the next week or so.  In
-the meantime, please use the current 
-<a href="develdownload.html">pre-release</a>
-for Isabelle 99.
-</p>
-<p>
-Some recent changes have been made to the support for
-<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>,
-so that it is easier to turn on and off, and support is now
-properly generic.  At the moment only Isabelle has 
-support implemented.
-</p>
-<li><b>21st October 1999</b><br>
- <p>
- See what Proof General 3.0 will look like!
- The <a href="screenshot.html">screenshot</a> has been updated.
- </p>
-<li><b>14th October 1999</b><br>
- <p>
- The next version of Proof General will be 3.0.
- </p>
- <p>
- There have been significant changes to the core of 
- Proof General and many improvements in the code.
- Extra features have been added, and the ones already
- there improved upon.  Usability has been a particular
- focus.  Adding new provers has been made easier.
- Installation will be made even easier.
- All of these changes warrant moving to a major release!
- </p>
- <p>
- Version 3.0 is planned for release in November.
- Please test a Version 3.0 pre-release if you can
- and report any problems.
- </p>
-<li><b>12th October 1999</b><br>
- <p>
- I'm very grateful to 
- <a href="mailto:courtieu@lri.fr">Pierre Courtieu &lt;courtieu@lri.fr&gt;</a>
- for offering to help work on Coq Proof General.
- <br>
- If anyone else in the Coq community would like to assist, please
- offer still, 
- there is plenty to do to add: better recognition of proof scripts,
- multiple file management, proof by pointing, etc...
- </p>
-<li><b>1st October 1999</b><br>
- <p>
- Recently there has been a flurry of work on the next version of Proof
- General.  It has quite a number of improvements (see the <?php
- fileshow("ProofGeneral/CHANGES","CHANGES"); ?> file), made by myself
- and Markus Wenzel.  <br> The next version is aimed to coincide 
- roughly with the release of Isabelle 99.
- </p>
- <p>
- At the moment we <b>urgently need</b> somebody from the Coq world to
- maintain and improve Coq Proof General, since Patrick Loiseleur 
- can no longer work on it.  
- Support from the Coq community is vital for Proof General to
- be a useful tool there. <a href="feedback">Please offer to help</a>, 
- it needn't be a heavy commitment.
- </p>
-<li><b>13th September 1999</b><br>
- <p>
- I've just returned from the 
- <a href="http://www-sop.inria.fr/types-project/types-sum-school.html">Types Summer School, Giens, France</a>
- where Proof General was used for a class of
- about 50 students who were learning
- Coq, Isabelle, and LEGO.  I received
- many useful comments and feedback,
- which will be
- used to improve the next version.
- Thanks to everyone who gave suggestions and bug reports
- to me, including: 
- Michael Abbott,
- Bernd Grobauer,
- Sebastian Skalberg,
- Thierry Massart,
- Darmalingum Muthiayen.
- <br>
- </p>
-<li><b>27th August 1999</b><br>
- <p>
- Print pictures from the new 
- <a href="gallery">gallery</a>
- of publicity shots of Proof General!
- </p>
-<li><b>24th August 1999</b><br>
- <p>
- Proof General version 2.1 is released.
- <br>
-  Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file
-  for a summary of changes since Proof General 2.0.
- </p>
- <p>
-  It is recommended that all users upgrade except
-  those still using Isabelle 98-1.  
-  <br> 
-  Proof General 2.1 supports only the 99 version of Isabelle.
- </p>
-</li>
-
-<li><b>24th June 1999</b><br>
-  <p>
-  New Proof General web pages go live!
-  </p>
-  <p>
-  The general is now more serious looking.
-  Appropriate, because there are some serious improvements 
-  in the pipeline...
-  Before that, we will release Proof General 2.1,
-  mainly a bug-fix improvement of 2.0.
-  </p>
-  <p>
-  Please explore the new web pages and report any problems 
-  or suggestions to <?php mlink($project_email); ?>.
-  Please also try out the latest pre-release of Proof General,
-  this is the final chance to get fixes and tweaks
-  sorted before 2.1.
-  </p>
-</li>
-
-<li><b>11th May 1999</b><br>
-  <p>A new instantiation of Proof General has been added by
-  <a href="http://www.dur.ac.uk/~dcs1pcc/">Paul Callaghan</a>
-  for 
-  <a href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a>,
-  a new proof assistant based on
-  Luo's Typed Logical Framework and
-  implemented in Haskell. 
-  </p>
-</li>
-
-<li><b>16th April 1999</b><br>
-  <p>A new instantiation of Proof General has been added by
-  <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>
-  for <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar</a>,
-  a new proof language for Isabelle to be included with Isabelle 99. 
-  </p>
-</li>
-</ul>
-<p>
-<i>News items by <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.</i>
-</p>
-
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/oldrel.php b/html/oldrel.php
deleted file mode 100644
index c48df091..00000000
--- a/html/oldrel.php
+++ /dev/null
@@ -1,162 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Previous Releases of Proof General"); 
-  ?>
-
-<p>
-Please note that we do not support these old releases in any way.
-</p>
-
-<h2>Proof General Version 3.3, released  10th September 2001</h2>
-<p>
-This version of Proof General has been tested
-with XEmacs 21.4 and (briefly) with GNU Emacs 20.7
-(it does <b>not</b> support GNU Emacs 21.x).
-It supports Coq version 7.x, LEGO version 1.3.1 and
-Isabelle2002.
-</p>
-
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.3.tar.gz") ?>,
-      <br>
-      or the same thing in a zip file:
-      <?php download_link("ProofGeneral-3.3.zip") ?>,
-  </li>
- <li> Linux RPM package:
-      <?php download_link("ProofGeneral-3.2-1.noarch.rpm") ?>
- </li>
-</ul>
-<p>
-Check the <?php fileshow("ProofGeneral-3.3/CHANGES","CHANGES"); ?> file
-for a summary of changes since version 3.2.
-</p>
-
-
-<h2>Proof General Version 3.2, released 2nd October 2000</h2>
-<p>
-This version of Proof General has been tested
-with XEmacs 21.1 and (briefly) with GNU Emacs 20.7.
-It supports Coq version 6.3, LEGO version 1.3.1 and
-Isabelle99-1.
-</p>
-
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.2.tar.gz") ?>,
-      <br>
-      or the same thing in a zip file:
-      <?php download_link("ProofGeneral-3.2.zip") ?>,
-  </li>
- <li> Linux RPM package:
-      <?php download_link("ProofGeneral-3.2-1.noarch.rpm") ?>
-     <br>
-     Also a
-      <?php download_link("ProofGeneral-3.2-1.src.rpm",
-	"source RPM") ?>.
- </li>
-</ul>
-<p>
-Check the <?php fileshow("ProofGeneral-3.2/CHANGES","CHANGES"); ?> file
-for a summary of changes since version 3.1.
-</p>
-
-<h2>Proof General Version 3.1, released 23rd March 2000</h2>
-
-<p>
-This version of Proof General has been tested
-with XEmacs 21.1 and GNU Emacs 20.4.
-It supports Coq version 6.3, LEGO version 1.3.1 and
-Isabelle99.
-</p>
-
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.1.tar.gz") ?>
-       <br>or zip file:
-      <?php download_link("ProofGeneral-3.1.zip") ?>,
-  </li>
-  <li> RPM package:
-      <?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?>
-     <br>
-     The 
-      <?php download_link("ProofGeneral-3.1-1.src.rpm",
-	"source RPM") ?>.
-   </li>
-</ul>
-<p>
-Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file
-for a summary of changes since version 3.0.
-</p>
-
-
-
-<h2>Proof General Version 3.0, released 26th November 1999</h2>
-
-<p>
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21.1.8 and GNU Emacs 20.5.<br>
-It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99.
-</p>
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.0.tar.gz") ?>
-  </li>
- <li> Linux RPM package:
-      <?php download_link("ProofGeneral-3.0-1.noarch.rpm") ?>
-     <br>
-     The source RPM is 
-      <?php download_link("ProofGeneral-3.0-1.noarch.rpm","here") ?>.
- </li>
-</ul>
-<p>
-Check the <?php fileshow("ProofGeneral-3.0/CHANGES","CHANGES"); ?> file
-for a summary of changes since version 2.1.
-</p>
-
-
-
-<h2>Proof General Version 2.1, released 24th August 1999</h2>
-
-<p>
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21 and GNU Emacs 20.3.<br>
-It supports Coq version 6.3, LEGO version 1.3.1 and
-some pre-release versions of Isabelle version 99.
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-2.1.tar.gz") ?>
-  </li>
- <li> Linux RPM package:
-      <?php download_link("ProofGeneral-2.1-1.noarch.rpm") ?>
-     <br>
-     The source RPM is 
-      <?php download_link("ProofGeneral-2.1-1.noarch.rpm","here") ?>.
- </li>
-</ul>
-
-
-<h2>Proof General Version 2.0, released 16th December 1998</h2>
-
-<p>
-This version of Proof General has been tested
-with XEmacs 20.4 and GNU Emacs 20.2, 20.3.<br>
-It supports Coq version 6.2, LEGO version 1.3.1, and
-Isabelle version 98-1.<br>
-</p>
-<ul>
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-2.0.tar.gz") ?>
-  </li>
- <li> Linux RPM package:
-      <?php download_link("ProofGeneral-2.0-1.noarch.rpm") ?>
-     <br>
-     The source RPM is 
-      <?php download_link("ProofGeneral-2.0-1.noarch.rpm","here") ?>.
- </li>
-</ul>
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/papers/pgoutline.pdf b/html/papers/pgoutline.pdf
deleted file mode 100644
index e712bade..00000000
--- a/html/papers/pgoutline.pdf
+++ /dev/null
diff --git a/html/papers/pgoutline.ps.gz b/html/papers/pgoutline.ps.gz
deleted file mode 100644
index 632f431a..00000000
--- a/html/papers/pgoutline.ps.gz
+++ /dev/null
diff --git a/html/papers/pgtalk.pdf b/html/papers/pgtalk.pdf
deleted file mode 100644
index 18989c20..00000000
--- a/html/papers/pgtalk.pdf
+++ /dev/null
diff --git a/html/papers/uitp03.pdf b/html/papers/uitp03.pdf
deleted file mode 100644
index ebcae29c..00000000
--- a/html/papers/uitp03.pdf
+++ /dev/null
diff --git a/html/projects.html b/html/projects.html
deleted file mode 100644
index ed2608d3..00000000
--- a/html/projects.html
+++ /dev/null
@@ -1,96 +0,0 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Projects"); 
-  ?>
-
-<p>
-Here are some proposals for projects connected to Proof General.
-</p>
-<p>
-The projects are designed as fairly self-contained contributions,
-involving code development and possibly a portion of supporting
-research.  They would be ideal projects for interested students
-or researchers.
-</p>
-<p>
-The projects are divided into those which are specific to Proof
-General, and those which would be useful more widely and do not depend
-on Proof General.  For more information on a project, click on its
-title.
-</p>
-
-<h2>A. Projects involving Proof General</h2>
-<ol>
-<li><?php pgproject("coqpbp","Proof-by-pointing support for Coq") ?></li>
-<li><?php pgproject("coqfile","Multiple file handling support for Coq") ?></li>
-<li><?php pgproject("isapbp","Proof-by-pointing support for Isabelle") ?></li>
-<li><?php pgproject("outline","Integrating block-structured development and outline mode") ?></li>
-<li><?php pgproject("thybrowse","A Generic Theory Browser") ?></li>
-<li><?php pgproject("pgml","Specification and tools for PGML") ?></li>
-<li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li>
-<li><?php pgproject("webreplay","A Web-based Proof Replayer for Proof General") ?></li>
-<li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li>
-<li><?php pgproject("hol","Proof General for HOL") ?></li>
-<li><?php pgproject("acs","Implementing Atomic Command Sequences") ?></li>
-<!-- <li><?php pgproject("pgkit","Proof General Kit (LFCS summer studentship)") ?></li> -->
-</ol>
-
-<h2>B. Projects not directly involving Proof General</h2>
-<ol>
-<li><?php pgproject("scrgen","Script General") ?></li>
-<!-- <li><?php pgproject("corba","An Experimental CORBA binding for ML") ?></li> -->
-<!-- <li><?php pgproject("reelcase","A ClearCase-like Configuration Management tool for Linux") ?></li> -->
-</ol>
-
-<p>
-Some projects involve Emacs Lisp.  This is the embedded programming
-language inside Emacs.  It is very easy to learn, since it is small,
-has a good manual, and has an interactive interpreter.  It is easy to
-use, not least because of its <i>self-documenting</i> nature: each
-variable or function is compiled together with documentation of its
-purpose.  (Other languages would do well to follow this).  It also
-has a powerful source-level debugger, <i>edebug</i>.
-</p>
-
-<!-- template for project pages -->
-<!-- <h2> </h2> -->
-<!-- <p> -->
-<!-- </p> -->
-<!-- <p> -->
-<!-- <b>Skills:</b> -->
-<!-- </p><p> -->
-<!-- <b>Proposer:</b> -->
-<!-- <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. -->
-<!-- </p> -->
-
-<p>
-If you are interested in working on any of these projects,
-feel free to discuss with the project proposer or on the 
-<a href="devel#develmail">developer's mailing list</a>.
-</p>
-
-<p>
-If you would like to use any of these ideas as a formal project
-proposal for students at your institution, please feel free
-but do <?php hlink("feedback","let us know ","Feedback form")?>
-if some work is begun, to help coordinate efforts.
-NB: the proposer of the project does not guarantee to be available for
-formal supervision or intensive help with the project (but it may be
-possible to find somebody else to do that).
-</p>
-
-<p>
-If you would like to submit a project proposal
-for an improvement or extension of Proof General,
-please send an email or write a description on the 
-<?php hlink("feedback","web feedback form","Feedback form")?>.
-Projects should be significant contributions rather than
-incremental improvements (although we welcome the suggestion of those
-too).
-</p>
-
-
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/projects/acs.html b/html/projects/acs.html
deleted file mode 100644
index d3768c17..00000000
--- a/html/projects/acs.html
+++ /dev/null
@@ -1,36 +0,0 @@
-<h2>Implementing Atomic Command Sequences</h2>
-<p>
-In Proof General, the blue region of a script buffer contains the
-initial segment of the proof script which has been processed
-successfully. It consists of atomic sequences of commands
-(ACS). Retraction is supported to the beginning of every ACS. By
-default, every command is an ACS. But the granularity of atomicity
-should be able to be adjusted.
-</p>
-<p>
-This adjustment is essential when arbitrary retraction is not
-supported in the prover. Usually, after a theorem has been proved, one
-may only retract to the start of the goal. One needs to mark the proof
-of the theorem as an ACS. At present, support for these goal-save
-sequences has been hard wired. No other ACS are currently
-supported. We need a generalisation to overcome this deficiency.
-</p>
-<p>
-This improvement should allow support for Coq's <i>Section</i> command,
-LEGO's <i>Discharge</i> and simplified support for Isabelle/Isar,
-by removing some of the prover-specific code.
-</p>
-<p>
-<b>References:</b>
-Proof General manual
-(<?php htmlshow("ProofGeneral/doc/ProofGeneral_17.html#SEC119","this section","Proof General Manual") ?>), and proof assistant manuals.</p>
-<p>
-<b>Skills:</b>
-Good Emacs Lisp, understanding of "granularity" problem
-for proof assistant history mechanisms.</p>
-<p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
-(based on an original idea by Thomas Kleymann).
-</p>
-
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html
deleted file mode 100644
index 35d48eb1..00000000
--- a/html/projects/coqfile.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<h2>Multiple file handling support for Coq</h2>
-<p>
-Coq Proof General does not yet handle script management across file
-boundaries, as do the LEGO and Isabelle versions.  Script management
-for multiple files means that whenever a file is viewed in the editor,
-it is locked if it has been loaded into the current Coq session.  It
-may mean that Proof General can make use of the file-level primitives
-of Coq, so that the user doesn't have to escape the interface, 
-or carefully load each file and its dependencies.  This also means that
-complete proof scripts will not so often need to be interpreted by
-Proof General, solving one of the present bottlenecks with using
-Coq Proof General.
-</p>
-<p>
-<b>Skills:</b>
- Some understanding of Coq implementation, co-operation with
- the Coq developers to get any Coq modifications (if any) incorporated.
- Some Emacs Lisp knowledge. 
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/coqpbp.html b/html/projects/coqpbp.html
deleted file mode 100644
index 366feb7c..00000000
--- a/html/projects/coqpbp.html
+++ /dev/null
@@ -1,17 +0,0 @@
-<h2>Proof-by-pointing support for Coq</h2>
-<p>
-Coq already has sophisticated notions of proof-by-pointing,
-and old work on support for Proof General may be helpful.  
-We want to integrate with the latest version of Coq's
-proof-by-pointing, possibly improving Proof General's
-support along the way.
-</p>
-<p>
-<b>Skills:</b>
- Some understanding of Coq implementation, co-operation with
- the Coq developers to get any Coq modifications (if any) incorporated.
- Minimal Emacs Lisp knowledge. 
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/corba.html b/html/projects/corba.html
deleted file mode 100644
index 35faa73f..00000000
--- a/html/projects/corba.html
+++ /dev/null
@@ -1,37 +0,0 @@
-<h2>An Experimental CORBA binding and IDL mapping for ML</h2>
-<p>
-The future version of Proof General may use CORBA as a communication
-mechanism between different components.  CORBA is also used by the
-Unix/Linux desktops KDE and GNOME, which use the free implementations
-MICO and ORBIT respectively.  We would like to be able to use ML to
-write to interface with other CORBA components on the desktop and 
-network.  For this a binding for ORB functions in ML is needed, as well 
-as perhaps a mapping from the CORBA IDL into Standard ML, so that
-we can write CORBA enabled applications in SML.  
-</p>
-<p>
-This project involves the design and implementation of an experimental
-version (subset of features) of such a system, using one of the
-open-source ML compilers such as Moscow ML, Poly/ML or OCaml (in fact,
-there is already some handling of COM in OCaml which can be used to
-access an ORB).  Essentially, we want to analyse the feasibility
-and performance of using a CORBA architecture for Proof General.
-</p>
-<p>
-An CORBA binding for Haskell would also be an interesting project.
-</p>
-<p>
-See 
-<a href="http://www.cl.cam.ac.uk/~cvr21/projects.html">Claudio Russo's</a> 
-project suggestion for a similar proposal, including useful links.
-</p>
-<p>
-<b>Skills:</b>
-Good ML, C, C++, programming skills and understanding of abstraction
-mechanisms, basic understanding of CORBA and willing to get to
-grasps with some of MICO or ORBIT.
-</p><p>
-<b>Proposers:</b>
-<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a> and
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/hol.html b/html/projects/hol.html
deleted file mode 100644
index 6828899a..00000000
--- a/html/projects/hol.html
+++ /dev/null
@@ -1,40 +0,0 @@
-<h2>Proof General for HOL</h2> 
-<p> 
-It is fairly easy to get basic support for Proof General for 
-<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL</a>, and
-this has recently been tried for HOL 98.  However, it would be a bigger
-and more interesting project to get proper and complete support for
-HOL working.  There are a couple of problems unique to HOL.
-</p>
-<p>
-Much more than Isabelle, HOL relies on its meta language, ML.  HOL
-proof scripts often use batch-oriented single step tactic proofs
-constructed in ML, but Proof General does not offer an easy way to
-edit these kind of proofs (as opposed to multi-step interactive
-proofs).  The <a
-href="http://hagi.is.s.u-tokyo.ac.jp/boomborg/">Boomburg-HOL</a> Emacs
-interface by Koichi Takahashi and Masima Hagiya addressed this
-problem, as well as providing support for proof-by-pointing to HOL.
-Their interface could perhaps be reinterpreted or reimplemented inside
-Proof General.  Implemented in a generic way, batch script editing
-would also be useful for Isabelle.
-</p>
-<p>
-Another problem is that HOL scripts sometimes use SML structures,
-which can cause confusion because Proof General does not really parse
-SML, it just looks for semicolons.  This could be improved by taking a
-better parser (e.g. from sml mode).
-</p>
-<p>
-Finally, to fully support the current Proof General feature set,
-it would be useful to extend HOL with support for communicating
-file-dependency information to Proof General, and term-structure
-markup for proof by pointing.
-<p>
-<b>Skills:</b>
-Some Standard ML, some Emacs Lisp.  Basic understanding of
-proof assistant behaviour, interest in HOL.  
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html
deleted file mode 100644
index c08ea85e..00000000
--- a/html/projects/isapbp.html
+++ /dev/null
@@ -1,25 +0,0 @@
-<h2>Proof-by-pointing support for Isabelle</h2>
-<p>
-Isabelle has a sophisticated concrete syntax mechanism which makes it
-difficult to add annotations to connect the displayed output back to
-the internal abstract syntax.  This issue needs to be solved to
-support proof-by-pointing (and other features) in Isabelle.
-A 
-<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
-patch by Burkhart Wolff</a> 
-providing term structure annotations for a previous release of
-Isabelle may be useful here.  To implement proof-by-pointing itself,
-tactics using the gesture information must be written.
-</p>
-<p>
-<b>Skills:</b>
- Some understanding of Isabelle implementation, 
- co-operation with the Isabelle developers to get
- Isabelle modifications incorporated.
- Skill in writing Isabelle tactics.
- Minimal Emacs Lisp knowledge.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
-
diff --git a/html/projects/outline.html b/html/projects/outline.html
deleted file mode 100644
index 67680b8f..00000000
--- a/html/projects/outline.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<h2>Integrating block-structured development and outline mode</h2>
-<p>
-Emacs already provides powerful outline facilities (cf. the
-outl-minor-mode setup for the well-known auc-tex package).  
-Similarly, proof systems such as Isabelle/Isar are inherently based on
-block-structured proof texts, with compositional proof checking.
-</p><p>
-But Proof General currently offers a mostly linear model of
-incremental script management.  The aim of this project is to extend that
-model to a hierarchic one: e.g. sub-proofs could be suppressed in the
-presentation, or even temporarily suspended (to achieve top-down
-development).
-</p><p>
-Outline support would be useful for the large scale structure of formal
-developments as well, e.g. support the basic arrangement into logical
-section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
-</p>
-<p>
-<b>Skills:</b>
-Some understanding of the workings of Emacs outline mode and Proof
-General script management.  Good portion of Emacs lisp knowledge.
-</p><p>
-<b>Proposer:</b>
-<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
-</p>
-
diff --git a/html/projects/pgip.html b/html/projects/pgip.html
deleted file mode 100644
index 073edd06..00000000
--- a/html/projects/pgip.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<h2>A New Protocol for Interactive Proof in Proof General</h2>
-<p>
-PGIP is a protocol for interactive proof to be used in the next
-version of Proof General.  It is based around the present protocol,
-but implemented with a standard collection of messages rather than
-different messages for different proof assistants.  An outline of PGIP
-and an experimental DTD
-is given in the <a href="/home/da/drafts/#white">white paper</a>.  A
-first implementation of PGIP will consist of (1) a filter (or
-modification of the output routines) for an existing proof assistant,
-which could be implemented in perl or some other language; and (2) a
-new backend for Proof General in Emacs, which configures it for PGIP.
-</p>
-<p>
-<b>Skills:</b>
-Interest in interactive proof and basic understanding
-of interaction mechanisms with at least one of 
-LEGO, Coq, Isabelle.   Programmming in Emacs Lisp.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/pgml.html b/html/projects/pgml.html
deleted file mode 100644
index 46cdd960..00000000
--- a/html/projects/pgml.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<h2>Specification and tools for PGML</h2>
-<p> 
-PGML is the proposed logical markup language for future versions of
-Proof General.  The basic version legitimizes the present markup
-scheme which is used by Proof General (based on 8-bit characters).
-The ideas for PGML are described in the white paper 
-<a href="/home/da/drafts/#white">here</a>, and an experimental
-DTD is given there.  This project is to refine the specification
-of PGML, and develop some tools for using it.  Various tools are desirable,
-including: (1) translation tools which convert PGML to various other
-formats, such as HTML and LaTeX.  (2) a display tool which displays PGML 
-inside Emacs, or converts it to HTML for display by a web browser; 
-(3) a filter or revised version of LEGO which converts its 8-bit markup 
-into PGML, for testing purposes.  We need the last tool for other
-proof assistants too.
-</p>
-<p> 
-<b>Skills:</b> 
-Understanding of markup languages and tools for using and specifying them.
-Interest in representation of mathematical content. 
-Necessary programming skills.
-</p><p> 
-<b>Proposer:</b> 
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p> 
-
diff --git a/html/projects/reelcase.html b/html/projects/reelcase.html
deleted file mode 100644
index f5fa2f04..00000000
--- a/html/projects/reelcase.html
+++ /dev/null
@@ -1,34 +0,0 @@
-<h2>A ClearCase-like Configuration Management tool for Linux</h2>
-<p>
-Managing large libraries of theories and proofs, good software
-engineering practices of configuration management become important
-when using proof assistants.  One powerful and popular configuration
-management tool is the commercial <a
-href="http://www.rational.com/products/clearcase/index.jtmpl">Rational
-ClearCase</a>.  
-</p>
-<p>
-The crucial way that ClearCase goes beyond CVS is in providing a view
-of a configuration directly through a special mountpoint on
-the filesystem.  
-</p>
-<p>
-This is a project to implement a kernel-level filesystem driver for
-Linux using the Linux VFS to create a ClearCase-like view of a
-configuration, through a mountable filesystem.  The underlying
-configuration management could be done through RCS or CVS, perhaps
-invoked via a companion user-level process.
-Particular revisions of files should be accessible through names
-interpreted specially by the filesystem driver, and some
-user-level commands will be needed for other operations.
-</p>
-<p>
-<b>Skills:</b> 
-Expert C programmer, with ability to understand and work on Linux
-kernel code.  Understanding of configuration management principles.
-</p><p>
-<b>Proposers:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
-from an idea by 
-<a href="http://www.dcs.ed.ac.uk/home/cxl">Christoph L&uuml;th</a>
-</p>
diff --git a/html/projects/scrgen.html b/html/projects/scrgen.html
deleted file mode 100644
index d65b477f..00000000
--- a/html/projects/scrgen.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<h2>Script General</h2>
-<p>
-Proof General is based around a core system of script management
-for proof scripts.  But the idea of script management is not
-restricted to proof assistants, it makes sense for many interactive
-scripting languages.  It deserves to be better known and used.
-A worthwhile project would be to rewrite the core script management
-features of Proof General so that they could work for arbitrary
-interactive scripting languages, and instantiate to Proof General as
-well as languages such as ML, Haskell, LISP, Scheme, Python, and
-even Emacs Lisp itself.
-</p>
-<p>
-An alternative version of this project is to implement a 
-generic basis for script management which does <i>not</i> depend on 
-Emacs, but uses a similar protocol to communicate with other
-text editors or display widgets.  This could be implemented in
-SML, OCaml, Java, C++, or any other suitable language.
-<p>
-<b>Skills:</b>
-Proficient Emacs Lisp (or other programming language), 
-knowledge of scripting languages desirable.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
diff --git a/html/projects/test.html b/html/projects/test.html
deleted file mode 100644
index f9d5ecf0..00000000
--- a/html/projects/test.html
+++ /dev/null
@@ -1,24 +0,0 @@
-<h2>A Test Harness and Test Suite for Proof General</h2>
-<p>
-As Proof General becomes a more complex system, we badly need some way
-of performing automatic functional testing, to ensure that changes and
-extensions preserve functional correctness.  Although classical
-testing of interfaces involves manually following a checklist of
-actions and observations, it should be straightforward to automate
-this using Emacs Lisp.  Interactive actions can be simulated by
-certain function calls, and their results can be determined by
-examining the contents of the edit buffers.  This project proposes the
-design and implementation of a test harness and accompanying test
-suite to test some of the core functions of Proof General.
-Ultimately, the tests should be run as part of the build process
-before each development release is allowed to go ahead.
-</p>
-<p>
-<b>Skills:</b>
-An interesting in testing user interfaces.
-Basic knowledge of Emacs Lisp.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
-
diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html
deleted file mode 100644
index 8993d942..00000000
--- a/html/projects/thybrowse.html
+++ /dev/null
@@ -1,34 +0,0 @@
-<h2>A Generic Theory Browser</h2>
-<p>
-Proof General has very limited mechanisms for helping the user find
-theorems and definitions during a proof.  It has notion of displaying
-a "current context" for a proof, and configuration with a proof
-engine command for searching for theorems.  It would be useful to
-extend these facilities with a <i>theory browser</i> for investigating
-the theories currently defined in (or available from) a running proof
-assistant.  This involves designing a small protocol to communicate
-with the proof assistant and a generic way of displaying theories
-which have different aspects from system to system.  A way which would
-fit in well with Emacs would be to use a <tt>dired</tt>-like buffer.
-</p>
-<p>
-An alternative version of this project would be to write a standalone
-theory browser which uses an extension of the forthcoming Proof
-General standardized protocol for interaction (see white paper <a
-href="/home/da/drafts/#white">here</a>).  This could be implemented in
-Java, or in a functional language, Perl, C or C++, so long as a nice
-toolkit is chosen (Qt or GTK).
-</p>
-<p>
-(For a related idea, see the browser integrated with OCaml).
-</p>
-<p>
-<b>Skills:</b>
-Interface programming skills.
-Basic understanding of what theories are for several different proof
-assistants.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
-
diff --git a/html/projects/webreplay.html b/html/projects/webreplay.html
deleted file mode 100644
index 1754e2df..00000000
--- a/html/projects/webreplay.html
+++ /dev/null
@@ -1,24 +0,0 @@
-<h2>A Web-based Proof Replayer for Proof General</h2>
-<p>
-One of the nice features of Proof General is that it is very easy to
-replay existing proofs, by mouse clicks alone.  No low-level
-understanding of a proof assistant is needed to step through proofs.
-We would like to have a web-based version of Proof General which
-allowed for this proof replay (at least), perhaps running a proof
-assistant remotely.  The main aspect is to implement an engine for
-script management (colouring of lines of files), displaying in a web
-browser, sending lines to a proof assistant process, and displaying the
-results.  Ideally, the ideas for new standard protocols for Proof
-General in the <a href="/home/da/drafts/#white">white paper</a> would
-be followed.
-</p>
-<p>
-<b>Skills:</b>
-Strong web programming skills using scripting languages,
-dynamic HTML, etc.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
-
-
diff --git a/html/projects/xmlpgip.html b/html/projects/xmlpgip.html
deleted file mode 100644
index 30828a97..00000000
--- a/html/projects/xmlpgip.html
+++ /dev/null
@@ -1,40 +0,0 @@
-<h2>A New Protocol for Interactive Proof in Proof General</h2>
-<p>
-PGIP is a protocol for interactive proof to be used in the next
-version of Proof General.  It is based around the present protocol,
-but implemented with a standard collection of messages rather than
-different messages for different proof assistants.  An outline of PGIP
-is given in the <a href="/home/da/drafts/#white">white paper</a>.  A
-first implementation of PGIP will consist of (1) a filter (or
-modification of the output routines) for an existing proof assistant,
-which could be implemented in perl or some other language; and (2) a
-new backend for Proof General in Emacs, which configures it for PGIP.
-</p>
-<p>
-<b>Skills:</b>
-Interest in interactive proof and basic understanding
-of interaction mechanisms with at least one of 
-LEGO, Coq, Isabelle.   Programmming in Emacs Lisp.
-</p><p>
-<b>Proposer:</b>
-<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-</p>
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-  <head>
-    <title></title>
-  </head>
-
-  <body>
-    <h1></h1>
-
-
-
-    <hr>
-    <address><a href="mailto:da@dcs.ed.ac.uk">David Aspinall</a></address>
-<!-- Created: Tue Apr 25 18:11:06 BST 2000 -->
-<!-- hhmts start -->
-Last modified: Tue Apr 25 18:22:01 BST 2000
-<!-- hhmts end -->
-  </body>
-</html>
diff --git a/html/proofgen.css b/html/proofgen.css
deleted file mode 100644
index 2cd91335..00000000
--- a/html/proofgen.css
+++ /dev/null
@@ -1,186 +0,0 @@
-/* Style sheet for the Proof General web pages. 
- * David Aspinall, June 1999.
- * proofgen.css,v 4.0 2000/03/13 07:36:57 da Exp
- */
-
-body{
- font-family: Verdana, Arial, sans-serif;	/* font for the doc body */
- background: #2D1D03;				/* background brown */
- background-image: 
-	url(images/canvaswallpaper.jpg);
- background-attachment: fixed;		/* background shouldn't scroll */
- color: #FFFFFF;		        /* text colour is white */
-}
-p{
- font-family: Verdana, Arial, sans-serif;	/* Netscape is picky, */
- color: #FFFFFF;			       /* so we must set every tag */
-}
-pre{
- font-family: LucidaTypewriter, monospace;
- color: #FFFFFF;
-}
-h1{
- font-family: Verdana, Arial, sans-serif;
- color: #FFFFFF;
- font-size: large;
- font-weight: bold;
-}
-h2{
- font-family: Verdana, Arial, sans-serif;
- font-size: medium;
- font-weight: bold;
- color: #FFFFD0;
- padding: 2px 4px 4px 4px;
- background: #7D4D33;
-}
-h3{
- font-family: Verdana, Arial, sans-serif;	
- font-size: medium;
- padding: 2px 2px 2px 2px;
- margin-right: 10%;
- background: #6D3D43;
- color: #FFFFD0;
-}
-h4{
- font-family: Verdana, Arial, sans-serif;	
- font-size: medium;
- color: #FFD0D0;
-}
-h5{
- font-family: Verdana, Arial, sans-serif;	
- font-size: medium;
- color: #E0C0C0;
-}
-
-blockquote,form,input,select{
- font-family: Verdana, Arial, sans-serif;	
- color: #FFFFFF;
-}
-
-address{
- font-family: Verdana, Arial, sans-serif;	
- font-size: small;				/* "smaller" is better on IE */
- color: #FFFFFF; 			       /* but varies randomly in NN */
-}
-
-select {
- font-family: Verdana, Arial, sans-serif;	
- font-size: 100%;
- background: #2D1D03;
- color: #FFFFFF;
-}
-
-textarea,input {
- font-family: Verdana, Arial, sans-serif;	
- font-size: 100%;
- background: #4D2D23;
- color: #FFFFFF;
-}
-
-input[type=submit],input[type=reset],input[type=Submit] {
- font-family: Verdana, Arial, sans-serif;
- font-size: 80%;
- padding-top: 0px;
- padding-bottom: 0px;
- background: #401010;
-}
-
-#button:active{
- background: #402020;
-}
-
-dl,ul,dir,li{
- font-family: Verdana, Arial, sans-serif;	
- color: #FFFFFF;
-}
-
-dt{ font-style: italic; 
-    padding: 2px 2px 2px 2px;
-    margin-left: 20px;
-    margin-right: 20px;
-    background: #6D3D43; 
-}
-
-table{
- font-family: Verdana, Arial, sans-serif;	
- color: #FFFFFF;
-}
-
-table.menubar{
- font-family: Verdana, Arial, sans-serif;	
- font-size: smaller;
- color: #FFFFFF;
-}
-
-
-
-
-td,tr{
- font-family: Verdana, Arial, sans-serif;	
-/* background-color: #2D1D03;   */
- color: #FFFFFF;
-}
-
-/* Link Elements */
-a:link,a:visited{					/* visited appears same */
- font-family: Verdana, Arial, sans-serif;	
- text-decoration: none;				/* Remove the underline */
- color: #FFD820;
-}
-
-/* hover is IE specific nasty but nice */
-a:active,a:hover{
- font-family: Verdana, Arial, sans-serif;	
- text-decoration: underline;			/* Underline on mouse over */
- color: #FFF030;				/* Brighter colour too */
-}
-
-
-pre{
- background: #2D1D03;
-}
-
-/* Specifics */
-
-p.nb{
- font-size: smaller;
- font-style: italic;
-}
-
-/* These bits for Mailman pages for mailing lists */
-TD.head1old {
- font-family: Verdana, Arial, sans-serif;
-  text-align: center;
-  color: #FFFFFF;
-  font-weight: bold;
-  font-size: 110%;
-}
-td.head1{
- font-family: Verdana, Arial, sans-serif;
- font-weight: bold;
- font-size: 110%;
- text-align: center;
- color: #FFFFFF;
-}
-td.head2{
- font-family: Verdana, Arial, sans-serif;
- font-size: 100%;
- font-weight: bold;
- color: #FFFFD0;
- padding: 2px 4px 4px 4px;
- background: #7D4D33;
-}
-td.head3{
- font-family: Verdana, Arial, sans-serif;	
- padding: 2px 2px 2px 2px;
- margin-right: 10%;
- background: #6D3D43;
- font-size: 80%;
- color: #FFFFD0;
-}
-td.head4{
- font-family: Verdana, Arial, sans-serif;	
- font-size: 100%;
- font-weight: bold;
- color: #FFD0D0;
-}
diff --git a/html/register b/html/register
deleted file mode 100644
index 5b5f0507..00000000
--- a/html/register
+++ /dev/null
@@ -1,108 +0,0 @@
-<?php  
-##
-##  Proof General registration form.
-##  
-##  David Aspinall, June 1999.
-##
-##  $Id$
-##
-  require('functions.php3');
-
-  $failure= ($argv[0]=="submit" && ($name=="" || $email=="" || $site==""));
-
-  if ($argv[0] !="submit" || $failure):
-###
-### Registration form
-###
-  small_header("Proof General Registration"); 
-
-  if ($failure):
-?>
-<p>
-  Your registration form was incomplete.  Please fill in all
-  the fields, thank-you!
-</p>
-<?php else: 
-  $mailinglist=true 
-?>
-<p>
-Please register your download using the short form below.  
-<br> 
-The information provided will only be used to help
-provide a case for support for Proof General in the future.
-</p>
-<p>
-If you have already registered you do not need to fill in the form
-again, so return to <a href="download#prereq">the download page</a>.
-</p>
-<?php endif; ?>
-<h2>Registration Form</h2>
-<form method=post action="<?php print $PHP_SELF . "?submit"; ?>">
-<table width="600" border="0" cellspacing="2" cellpadding="0">
-<tr>
- <td width="30%">Your name:</td>
- <td width="70%"><input type=text name="name" size="40" 
-		  value="<?php echo $name;?>"></td>
-</tr>
-<tr>
- <td width="30%">Email address:</td>
- <td width="70%"><input type=text name="email" size="40"
-		  value="<?php echo $email;?>"></td>
-</tr>
-<tr>
- <td width="30%">Your site name:</td>
- <td width="70%"><input type=text name="site" size="40"
-		  value="<?php echo $site;?>"></td>
-</tr>
-<tr>
- <td width="30%"><input type=checkbox name="mailinglist"
-		  <?php if ($mailinglist) print "checked"; ?>></td>
- <td width="70%">Please add me to the mailing list.</td>
-</table>
-<br>
-<input type=submit value="Send form"> 
-</form>
-<?php  
-   click_to_go_back(); 
-   footer(); 
-  else:
-##
-##  Process registration
-##
-   small_header("Registration Form Sent");
-
-
-   $message = "Registration form for using Proof General" 
-	    . "\nName:\t\t " . $name
-	    . "\nEmail:\t\t " . $email
-	    . "\nSite:\t\t " . $site
-	    . "\nSubmitted:\t" . date("h:ia D jS F Y");
-   mail("proofgen@dcs.ed.ac.uk",
-	"[Registration form from ~proofgen]",
-	 $message);
-   
-   print "<p>Dear " . $name . ",</p>\n"; 
-   print "<p>";
-   print "Thank you for filling in the form. Your registration has been sent.<br>";
-
-   /* Next bit duplicated in mailinglist.html.  
-      Could be a function in functions.php3 */
-
-   if ($mailinglist) {
-	$message = "subscribe address=$email"; 
-	mail("proofgeneral-request@informatics.ed.ac.uk",
-	     "[Web form from Proof General]",
-	     $message,
-	    "Reply-To: " . $email . "\nFrom: " . $email);
-        print "A subscription request has been sent for the Proof General mailing list.<br>";
-   }
-   print "</p>\n<p>";
-
-   print "<p>\nClick ";
-   print "<a href=\"download#prereq\">here</a>";
-   print " to return to the download page.<br></p>\n";
-   click_to_go_back();
-  
-   footer();
- endif;
-?>
diff --git a/html/register.html b/html/register.html
deleted file mode 100644
index 4fe35617..00000000
--- a/html/register.html
+++ /dev/null
@@ -1,110 +0,0 @@
-<?php  
-##
-##  Proof General registration form.
-##  
-##  David Aspinall, June 1999.
-##
-##  $Id$
-##
-  require('functions.php3');
-
-  $failure= ($argv[0]=="submit" && ($name=="" || $email=="" || $site==""));
-
-  if ($argv[0] !="submit" || $failure):
-###
-### Registration form
-###
-  small_header("Proof General Registration"); 
-
-  if ($failure):
-?>
-<p>
-  Your registration form was incomplete.  Please fill in all
-  the fields, thank-you!
-</p>
-<?php else: 
-  $mailinglist=true 
-?>
-<p>
-Please register your download using the short form below.  
-<br> 
-The information provided will only be used to help
-provide a case for support for Proof General in the future.
-</p>
-<p>
-If you have already registered you do not need to fill in the form
-again, so return to <a href="download#prereq">the download page</a>.
-</p>
-<?php endif; ?>
-<h2>Registration Form</h2>
-<form method=post action="<?php print $PHP_SELF . "?submit"; ?>">
-<table width="300" border="0" cellspacing="2" cellpadding="0">
-<tr>
- <td width="30%">Your name:</td>
- <td width="70%"><input type=text name="name" size="40" 
-		  value="<?php echo $name;?>"></td>
-</tr>
-<tr>
- <td width="30%">Email address:</td>
- <td width="70%"><input type=text name="email" size="40"
-		  value="<?php echo $email;?>"></td>
-</tr>
-<tr>
- <td width="30%">Site name:</td>
- <td width="70%"><input type=text name="site" size="40"
-		  value="<?php echo $site;?>"></td>
-</tr>
-<tr>
- <td width="30%"><input type=checkbox name="mailinglist"
-		  <?php if ($mailinglist) print "checked"; ?>></td>
- <td width="70%">Please add me to the mailing list.</td>
-</table>
-<input type=submit value="Send form"> 
-</form>
-<p>
-</p>
-<?php  
-   click_to_go_back(); 
-   footer(); 
-  else:
-##
-##  Process registration
-##
-   small_header("Registration Form Sent");
-
-
-   $message = "Registration form for using Proof General" 
-	    . "\nName:\t\t " . $name
-	    . "\nEmail:\t\t " . $email
-	    . "\nSite:\t\t " . $site
-	    . "\nSubmitted:\t" . date("h:ia D jS F Y");
-   mail("da+pg-register@inf.ed.ac.uk",
-	"[Registration form from ~proofgen]",
-	 $message);
-   
-   print "<p>Dear " . $name . ",</p>\n"; 
-   print "<p>";
-   print "Thank you for filling in the form. Your registration has been sent.<br>";
-
-   /* Next bit duplicated in mailinglist.html.  
-      Could be a function in functions.php3 */
-
-   if ($mailinglist) {
-	$message = "subscribe proofgeneral"; 
-	mail("mailman@inf.ed.ac.uk",
-	     "[Web form from ~proofgen]",
-	     $message,
-	    "Reply-To: " . $email . "\nFrom: " . $email);
-        print "Your name has been added to the Proof General mailing list.<br>";
-   }
-   print "</p>\n<p>";
-
-   print "<p>\nClick ";
-   print "<a href=\"download#prereq\">here</a>";
-   print " to return to the download page.<br></p>\n";
-   click_to_go_back();
-  
-   footer();
- endif;
-?>
-
diff --git a/html/robots.txt b/html/robots.txt
deleted file mode 100644
index 855ec318..00000000
--- a/html/robots.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-# robots.txt for http://proofgeneral.inf.ed.ac.uk
-# see http://httpd.apache.org/docs/misc/howto.html
- 
-User-agent: *
-Disallow: /cgi/ # cgi scripts
-# Disallow: /manual/ # get it somewhere else
diff --git a/html/screenshot b/html/screenshot
deleted file mode 100644
index bba013ba..00000000
--- a/html/screenshot
+++ /dev/null
@@ -1,8 +0,0 @@
-<?php require('functions.php3'); ?>
-<?php  include('head.html'); ?>
-<?php
-    include('header.html');
-    include($WANTED . '.html');
-    footer();
-?>
-
diff --git a/html/screenshot.html b/html/screenshot.html
deleted file mode 100644
index ffc9e8a4..00000000
--- a/html/screenshot.html
+++ /dev/null
@@ -1,115 +0,0 @@
-<p>
-Here are some screenshots of Proof General 3.0 running with
-different theorem provers.  To see the full-size version
-of a picture, click on its thumbnail.
-</p>
-
-<!-- FIXME: update pictures.  Fix vertical centering of screenshots. -->
-
-<table width="80%">
-<tr>
-<td width="200">
-<a href="images/pg-lego-screenshot.png">
-<img src="images/pg-lego-thumb.png" alt="LEGO Proof General" width=128 height=109 border=0>
-</a>
-</td>
-<td>
-<p><font size="-1">
-Building a simple proof in LEGO with proof-by-pointing.
-<br>
-The top half of the window displays the proof script. 
-The bottom displays the output from LEGO at each
-stage of the proof.  Here, it shows
-the current subgoals to be solved.
-The part of the proof already processed by LEGO
-has a blue background.
-<br>
-Clicking on terms in the subgoals list generates
-commands which are added to the proof script.
-</font></p>
-<br>
-</td></tr>
-
-<tr>
-<td width="200">
-<a href="images/pg-coq-screenshot.png">
-<img src="images/pg-coq-thumb.png" alt="Coq Proof General" width=153 height=115 border=0>
-</a>
-</td>
-<td>
-<p><font size="-1">
-Coq Proof General running in multiple frame mode,
-full screen shot (1024x768).
-<br>
-There are separate windows on the screen
-for the script, goals, and response buffers.
-In this picture, you can see Proof General's
-indication that Coq is processing the
-induction step, because the background of
-the proof step is pink.  It will become
-blue when Coq finishes that step.
-</font></p>
-<br>
-</td></tr>
-
-<tr>
-<td width="200">
-<a href="images/pg-isa-screenshot.png">
-<img src="images/pg-isa-thumb.png" alt="Isabelle Proof General" width=150 height=142 border=0>
-</a>
-</td>
-<td>
-<p><font size="-1">
-Replaying a domain theory proof in Isabelle's HOLCF logic.
-<br>
-In Isabelle, theory files as well as ML files are coloured.
-Proof General has some functions for processing and
-undoing theory files, but most operations it provides
-are for writing proof scripts in ML files.
-<br>
-Isabelle supports input and output in tokens which
-display as symbols using the 
-<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
-package in conjunction with Proof General.  
-Here you can see some symbols in Isabelle's output.
-</font></p>
-<br>
-</td></tr>
-
-<tr>
-<td width="200">
-<a href="images/pg-isar-screenshot.png">
-<img src="images/pg-isar-thumb.png" alt="Isabelle/Isar Proof General" width=150 height=142 border=0>
-</a>
-</td>
-<td>
-<p><font size="-1">
-Replaying a proof in Isar, Isabelle's declarative proof language
-developed by Markus Wenzel.
-</font></p>
-<br>
-</td></tr>
-
-<tr>
-<td width="200">
-<a href="images/pg-lego-console.png">
-<img src="images/pg-lego-console-thumb.png" alt="LEGO Proof General (console)" width=174 height=65 border=0>
-</a>
-</td>
-<td>
-<p><font size="-1">
-LEGO Proof General running in plain console mode.
-<br>
-This shows that you can run Proof General even if sometimes
-you need to use a plain tty or xterminal.   Of course, the
-graphical features are reduced!
-</font></p>
-<br>
-</td>
-</tr>
-</table>
-
-<p>
-For more pictures, see the Proof General <a href="gallery">gallery</a>.
-</p>
-
diff --git a/html/smallheader.html b/html/smallheader.html
deleted file mode 100644
index ade4e6dd..00000000
--- a/html/smallheader.html
+++ /dev/null
@@ -1,8 +0,0 @@
-<table width="80%">
-<tr>
-<td width="15%">
-<a href="">
-<img src="images/PG-small.jpg" align=top width=37 height=50 border=0 alt="Proof General Home">
-</a>
-</td>
-<td width="85%">
diff --git a/html/smallpage.html b/html/smallpage.html
deleted file mode 100644
index 64f538a3..00000000
--- a/html/smallpage.html
+++ /dev/null
@@ -1,6 +0,0 @@
-<?php
-  require('functions.php3');
-  small_header($title);
-  include($file);
-  footer(); 
-?>
diff --git a/html/smallpage.php b/html/smallpage.php
deleted file mode 100644
index ef165c6d..00000000
--- a/html/smallpage.php
+++ /dev/null
@@ -1,12 +0,0 @@
-<?php
-  require('functions.php3');
-  small_header($title);
-  if (substr($file,0,1)=="." or 
-      substr($file,0,1)=="/" or
-      substr($file,0,1)=="~") {
-     print "Sorry, can't show you that file!\n"; 
-  } else {
-    include($file);
-  }
-  footer(); 
-?>
diff --git a/html/userman b/html/userman
deleted file mode 100644
index e8ccc072..00000000
--- a/html/userman
+++ /dev/null
@@ -1,3 +0,0 @@
-<?php require('functions.php3');
-      hack_html("ProofGeneral/doc/ProofGeneral_toc.html","Proof General user manual","userman");
-?>