From 670761dd6bd6321d65beeacdc81d68c0a2ebe92b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 13 Mar 2000 05:14:23 +0000
Subject: Updated web pages.

---
 html/projects/hol.html | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'html/projects')

diff --git a/html/projects/hol.html b/html/projects/hol.html
index 4b623bfb..6828899a 100644
--- a/html/projects/hol.html
+++ b/html/projects/hol.html
@@ -26,9 +26,14 @@ 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.
+proof assistant behaviour, interest in HOL.  
 </p><p>
 <b>Proposer:</b>
 <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
-- 
cgit v1.2.3