Deleted file

1 files changed, 0 insertions, 40 deletions

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>