Updated

3 files changed, 39 insertions, 28 deletions

diff --git a/CHANGES b/CHANGES
index 6f7ea1f4..e03c3ca0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,8 +3,25 @@
 * Summary of Changes for Proof General 3.1 from 3.0
 
 
+** New instantiations of Proof General!
+
+*** HOL 98 (http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html)
+
+   by David Aspinall.  This is a bare-bones Proof General instance
+   only, hopefully to entice HOL users so that someone may improve it.
+   See README in the hol98 directory for more details.
+
+*** Plastic (http://www.dur.ac.uk/CARG/plastic.html)
+  
+   by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
+   The Plastic system itself is not yet publicly available,
+   so this is only included in the developers tar file.
+
+
 ** Generic Changes
 
+*** README file added for each supported prover, explaining support.
+
 *** Fixes for supporting Japan versions of Emacs which have older CL macs.
  
   CL macs with Japanicised documentation, defined in "egg.el".
@@ -49,22 +66,11 @@
 *** Minor syntax tweaks.
 
 
+** Changes for developers to note
 
-** New instantiations of Proof General for:
-
-*** Plastic (http://www.dur.ac.uk/CARG/plastic.html)
-  
-   by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
-   The Plastic system itself is not yet publicly available.
-
-*** HOL 98 (http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html)
-
-   by David Aspinall.  This is a bare-bones Proof General instance
-   only, hopefully to entice HOL users so that someone may improve it.
-   See README in the hol98 directory for more details.
+*** todo file added for each prover, split from global todo file
 
 
-** Changes for developers to note
 
 
 
diff --git a/isa/todo b/isa/todo
index b5b4ad04..da20d04a 100644
--- a/isa/todo
+++ b/isa/todo
@@ -5,6 +5,20 @@
 * Things to do for Isabelle
 ===========================
 
+C Investigate fix for looping rewriting in Isabelle.  Continual
+  and frequent messages from the prover lock out the user.
+  Is there any easy way of fixing this?
+  
+C X-Symbol support for theory files: bugs at the moment, because
+  of duplicate calls to proof-x-symbol-mode and mess with
+  font-lock initialization.  Problem with current version:
+  visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
+  Seems okay visiting new buffers after that.
+  Must also check interaction with xsym-isa-latex stuff
+  may be broken by removal of mode hook settings.
+  [DvO reports okay].
+  (May need to split extra modes into two parts?)
+
 B auto-adjust Pretty.setmargin when window is resized.  Use
   generic code once it's implemented.
 
diff --git a/todo b/todo
index c4dd6548..43c6219d 100644
--- a/todo
+++ b/todo
@@ -38,7 +38,8 @@ X (Low)		e.g. probably not worth spending time on
 
 ** Isabelle regexp overflow problem on proof-shell-proof-completed-regexp
 ** Solaris ^G problem and FSF Emacs mule/non-mule support
-** Recognition of ; only at eol (DvO reported bug)
+** Recognition of ; only at eol (DvO reported bug here, shouldn't happen)
+** Web page: add notify when updated option
 
 
 * Scheduled improvements for 3.2
@@ -54,6 +55,10 @@ X (Low)		e.g. probably not worth spending time on
 * Things to in the generic interface
 ====================================
 
+C More flexible help configuration is needed.  HOL has some nice
+  on-line help but no way in PG to help by library.  Perhaps
+  a help browser is needed?
+
 B Manual improvements before techreport publishing (see notes at end also):
   - Mention configuring function menus, outline.
   - Consider splitting up chapter 9?
@@ -65,24 +70,10 @@ B Manual improvements before techreport publishing (see notes at end also):
   - add screenshots?
   - add more index entries
 
-C X-Symbol support for theory files: bugs at the moment, because
-  of duplicate calls to proof-x-symbol-mode and mess with
-  font-lock initialization.  Problem with current version:
-  visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
-  Seems okay visiting new buffers after that.
-  Must also check interaction with xsym-isa-latex stuff
-  may be broken by removal of mode hook settings.
-  [DvO reports okay].
-  (May need to split extra modes into two parts?)
-
 C Investigate support under Mule.  Suggestion we need to set
   process-coding-system-alist somehow to prevent coding.
   What about Mew ?
 
-C Investigate fix for looping rewriting in Isabelle.  Continual
-  and frequent messages from the prover lock out the user.
-  Is there any easy way of fixing this?
-  
 D Change the name of "automatic multiple files" to something
   more comprehensible.