diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-10 08:52:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-10 08:52:19 +0000 |
| commit | e7e378ec259c1e545ac1adbc8b0c46faf7747f83 (patch) | |
| tree | 6f4a15a5e67dfda253f6786801df55ab96aa26bf | |
| parent | b0856d2da99b62ca6f33528d6e01bfd604e39958 (diff) | |
News about HOL support.
| -rw-r--r-- | html/news.phtml | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/html/news.phtml b/html/news.phtml index f54654d5..9131d56b 100644 --- a/html/news.phtml +++ b/html/news.phtml @@ -6,6 +6,30 @@ </p> <ul> +<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/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> +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.phtml">development release</a>. +</p> <li><b>15th February 2000</b> <p> There is now a new |