Updated

2 files changed, 32 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index cb525b06..f429b19b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,7 +4,7 @@
 
 ----- NB: this is a pre-release of PG 3.2.  Bugs likely, please report ------ 
 
-
+----- PG 3.2 is scheduled for release in Autumn 2000. -----
 
 ** Generic Changes
 
@@ -47,12 +47,13 @@
 
 *** Bug fix: first line ignored problem fixed for Coq and others.
  
-  To fix this properly, we have added `proof-shell-pre-sync-init-cmd'
-  for provers that need initialization before synchronization can be
-  secured.  [Developers note: LEGO needs to wait for second prompt
-  before sync, whereas Isabelle managed to sync on first prompt.  
-  Coq was best, with sync set before startup, using a command line option.
-  That is the recommended route for new proof assistants.]
+  [Developers note: to fix this properly, we have added
+   `proof-shell-pre-sync-init-cmd' for provers that need initialization
+   before synchronization can be secured.  LEGO needs to wait for
+   second prompt before sync, whereas Isabelle managed to sync on first
+   prompt.  Coq was best, with sync set before startup, using a command
+   line option.  That is the recommended route for new proof
+   assistants.]
 
 *** Bug fix: script management is now more robust against C-x C-v, C-x C-w
 
@@ -62,12 +63,12 @@
 
   Specific menus added for Coq, LEGO, Isabelle.
 
-*** Favourites: user-defined commands added proof assistant specific menu
-
 *** Proof assistant specific keymap added
 
   Keybindings for proof assistant now begin with "C-c C-a".
 
+*** Favourites: user-defined commands can be added to PA-specific menu.
+
 *** Improved behaviour of electric terminator
 
 *** Quick menu option to select proof-follow-mode
diff --git a/todo b/todo
index 4914f320..aaffc97d 100644
--- a/todo
+++ b/todo
@@ -998,20 +998,37 @@ Output written on ProofGeneral.pdf (2 pages, 54702 bytes).
 *** A Try to get small project grant from LFCS to help with
   development of Proof General.  Latest news: success is 
   doubtful. Needs a self-contained project that 
-  *would be useful to LFCS*
+  *would be useful to LFCS*.  
+  One idea: an LFCS CDROM featuring Proof General and 
+  bundled with other theorem provers?    How much does a 
+  short-run (200 CDs?) cost?
+
+*** A 
+
+*** A Write grant proposal on white paper for Proof General Kit.
 
 *** A Find new people to help advance and develop Proof General.
   Getting more instances would be a good way.  Also encouraging
-  feedback.  Here stories of bugs by word-of-mouth, they don't
+  feedback.  Hear stories of bugs by word-of-mouth, they don't
   get reported often enough.
   Consider passing on project elsewhere if no LFCS interest.
 
-*** A Polish ProofGeneral.texi and publish LaTeX as a tech report
+*** A Polish ProofGeneral.texi and publish as a tech report
+  For PG 3.2, probably.  
 
 *** A Write paper on design and development of Proof General.
 
 *** A Write white paper on future of PG project.
 
-*** A Write grant proposal on white paper for Proof General Kit.
+*** A Add more PG projects, publicise them.
+
+*** A Push PG research directions:
+	- configuration management / dependency organization
+	- ideas about proof engineering cf software engineering
+	- research on ways of conducting a formalization, cf
+	  ways of writing a program.  Common idioms that PG could
+	  help with.
+
+*** A Add instructions for developers to use cvs repository 
+    remotely.
 
-*** A Add more PG projects, ensure interest is generated!