Updates

1 files changed, 16 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index 960aae1b..0d493981 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,10 +17,12 @@ It is now permitted to use Proof General in any context, without
 applying for a special license from University of Edinburgh.  
 Free redistribution is also allowed under the GPL conditions.
 
-*** Remove handling for provers you don't want
+*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X
 
-You can simply remove the directories from the PG distribution,
-instead of customizing the `proof-assistants' variable.
+Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs.  
+
+Sorry, this version of PG does not support Emacs 20; backwards
+compatibility is far too difficult to maintain.
 
 *** Colours altered
 
@@ -28,14 +30,15 @@ Queue and locked colours made a little less lurid.
 (Look in proof-config for proof-locked-face, proof-queue-face
 and old settings if you want to change back).
 
-*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X
+*** Improvements to visibility controls
 
-Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs.  
+Visibility controls now work for comments and commands in proof
+scripts.  An image is used in XEmacs to signal hidden text.
 
-Sorry, this version of PG does not support Emacs 20; backwards
-compatibility is far too difficult to maintain.
+*** Improvement to "Favourites" user-defined menus 
 
-*** Improvement to "Favourites" user-defined menus (deletion added)
+Favourites are now more robust.  You can delete them and save them
+when you want.
 
 *** Support for "tracing" buffers improved and enabled by default.
 
@@ -44,6 +47,11 @@ Compared with experimental tracing in PG 3.3, there is now only one
 tracing buffer, treated somewhat like a response buffer.
 For minor issues, see isa/BUGS.
 
+*** Easily remove handling for provers you don't want 
+
+You can simply remove the directories from the PG distribution,
+instead of customizing the `proof-assistants' variable.
+
 
 
 ** Isabelle Changes