diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 05:14:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 05:14:23 +0000 |
| commit | 670761dd6bd6321d65beeacdc81d68c0a2ebe92b (patch) | |
| tree | 42cb0879a750de1af1122ab103272f305ad5902e /html/projects | |
| parent | 5e9f920b0d834276ed2df4db60f95357460818bd (diff) | |
Updated web pages.
Diffstat (limited to 'html/projects')
| -rw-r--r-- | html/projects/hol.html | 7 |
1 files changed, 6 insertions, 1 deletions
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>. |