Updated

2 files changed, 14 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 42e74a44..7ebbb4da 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,18 +18,30 @@
 
 *** Added possibility for switching prover's output on/off.
 
+  Already implemented in Coq and Isabelle(/Isar).
+
 
 ** Coq Changes
 
+*** More decoration of Coq output, uses CoqResp mode now
+
 ** LEGO Changes
 
+*** Slight change in output during proof: show final discharge messages
+
 ** Isabelle Changes
 
 *** Fix for stack overflow in regexp which occurred with large proof states
 
 ** Isar Changes
 
+** HOL Changes
+
+*** Output decoration improvements.
+
 ** Changes for developers to note
 
 *** No need for match string 1 in proof-shell-proof-completed
 
+*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.
+
diff --git a/todo b/todo
index ddbc5e6b..d895c997 100644
--- a/todo
+++ b/todo
@@ -29,7 +29,7 @@ X (Low)		e.g. probably not worth spending time on
 
 *** Scheduled improvements for 3.2
 
-**** A Doc new bits: font lock keywords, silent stuff, filename %e, %r.
+**** A Doc new bits: font lock keywords, filename %e, %r.
 
 **** A Add a new keymap(s) for proof assistants.
   Presently they naughtily bind C-c <letter> which are reserved for
@@ -42,7 +42,7 @@ X (Low)		e.g. probably not worth spending time on
 
 **** A Add efficiency improvement by turning on/off prover output.
   Patch already added to pre-release.
-  Needs adjusting to turn on output in case of error/interrupt.
+  Does it need adjusting to turn on output in case of error/interrupt?
 
 **** C Add improvements to script movement in electric terminator mode.
   Some commented regions in code.  E.g. automatic newline/space after