2 files changed, 94 insertions, 78 deletions
diff --git a/html/news.phtml b/html/news.phtml
index 3e02577d..ac7d4054 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -6,91 +6,28 @@
 </p>
 
 <ul>
-<li><b>23rd March 2000</b>
-<p>
-Proof General 3.1 is now available from the
-<?php link_root("download","download page") ?>.  Enjoy!
-</p>
-</li>
-<li><b>14th March 2000</b>
+<li><b>4th April 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.
+A minor patch to Proof General 3.1 is released today.  To check what
+version you have, look at the variable <tt>proof-general-version</tt>
+set in <tt>proof-site.el</tt>.  (It is not recorded in the tar file
+name or package version).  The current patch, to 3.1.3, was made to
+fix a problem with Isabelle and theory file retraction, accidently
+introduced in 3.1.  See <?php
+fileshow("ProofGeneral-3.1-devel/etc/release-log.txt","the developer's
+release log"); ?> for details.
 </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.
+Further improvements are being introduced in the new 3.2 pre-releases,
+see the 
+<a href="develdownload.phtml">development download</a> page, as usual.
 </p>
+<li><b>23rd March 2000</b>
 <p>
-The HOL support is shipping in the 
-current <a href="develdownload.phtml">development release</a>.
+Proof General 3.1 is now available from the
+<?php link_root("download","download page") ?>.  Enjoy!
 </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>
 </ul>
 <p>
 <i>Click <a href="oldnews.phtml">here</a> for old news.</i>
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