Updated

1 files changed, 17 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index a7567eaf..3dc8b5f7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,7 +8,7 @@
 
 ** Generic Changes
 
-*** Proof assistant specific menus.  
+*** Menu reorganization, including new proof assistant specific menus.  
 
   Specific menus added for Coq, LEGO, Isabelle.
 
@@ -22,6 +22,8 @@
 
 *** Improved behaviour of electric terminator
 
+*** Quick menu option to select proof-follow-mode
+
 *** Point never moves if proof-follow-mode is 'ignore.
 
   Previously it was always moved when an error occurred.
@@ -72,7 +74,21 @@
       ;;;###autoload comments with `make devel.autoloads'
 
       Several new files, to "modularize" the code a bit more.
+
+*** New mechanism for defining customizations per prover
+
+      See Section 9 of proof-config.el.  New macros mean that we can
+      write for example `proof-defasscustom web-page' to automatically get 
+      `isa-webpage', `hol-webpage', etc, declared on loading.
       
+      Proof assistant specific code can then just set/use these
+      variables, without needing to set `proof-assistant-webpage' from
+      `isa-webpage' etc.
+
+      This slightly breaks the original pseudo object-oriented idea
+      behind the instantiation mechanism (overriding methods, setting
+      attributes) but works much more smoothly with customization.
+
 
 *** No need for match string 1 in proof-shell-proof-completed