Deleted file

1 files changed, 0 insertions, 26 deletions

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> 
-