From e7e378ec259c1e545ac1adbc8b0c46faf7747f83 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 10 Mar 2000 08:52:19 +0000
Subject: News about HOL support.

---
 html/news.phtml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'html')

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 
-- 
cgit v1.2.3