Updated news about 3.1.3, split old news out.

1 files changed, 79 insertions, 0 deletions

diff --git a/html/oldnews.phtml b/html/oldnews.phtml
index 13d16fd2..182653f2 100644
--- a/html/oldnews.phtml
+++ b/html/oldnews.phtml
@@ -3,6 +3,85 @@
   small_header("Proof General Old News"); 
   ?>
 <ul>
+<li><b>14th March 2000</b>
+<p>
+Release candidate for Proof General 3.1 available.
+Pre-releases from now on are release candidates for version 3.1.
+Please test and report any problems you find
+(check the CHANGES and BUGS lists for issues known about
+and/or resolved).  Version 3.1 should be released next week.
+</p>
+</li>
+<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/Researc/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>
+<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>
+<li><b>15th February 2000</b>
+<p>
+There is now a new 
+<?php link_root("devel","page for developers") ?>.
+I plan to apply for funding to continue managing the evolution
+and development of Proof General, once my own job position
+is more secure.  
+Now is the time to flesh out ideas
+for the future!  
+Check the development page for the
+latest proposals.  These include some desirable contributions 
+which could be undertaken as self-contained projects.
+</p>
+<li><b>9th February 2000</b>
+<p>
+Countdown to Proof General 3.1 begins.  This will be a bug fix releaase.
+A few bugs have been fixed in
+recent Proof General development releases, one important one is fixing
+support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu
+for raising it to my attention).  I would like to release PG 3.1 next
+month so that everyone can benefit.
+</p>
+<p>
+In the meantime, please 
+<?php 
+  hlink("feedback.phtml","report any important problems ","Feedback form")?>
+that you would like to see fixed, and consider trying out 
+the current <a href="devel.phtml">development release</a>.
+</p>
+<li><b>14th December 1999</b>
+<p>
+I'm pleased to say that Proof General will be demonstrated at
+<a href="http://iks.cs.tu-berlin.de/etaps2000/etaps.html">ETAPS 2000</a>.
+Here are some draft <a href="papers/pgtalk.pdf">slides</a> for 
+the presentation 
+(any <a href="mailto:da@dcs.ed.ac.uk">comments</a> would be welcome).
+A presentation of Proof General based on these slides was given at 
+<a href="http://www.clrc.ac.uk/">Rutherford Appleton Laboratory</a> last week.
+</p>
+<li><b>26th November 1999</b>
+<p>
+Proof General 3.0 is released!
+</p>
 <li><b>17th November 1999</b><br>
 <p>
 Proof General 3.0 is currently in final testing, and will be released