1.1 --- a/NEWS	Tue Sep 02 22:37:20 2008 +0200
     1.2 +++ b/NEWS	Tue Sep 02 22:41:36 2008 +0200
     1.3 @@ -180,6 +180,11 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Generic Toplevel.add_hook interface allows to analyze the result of
     1.8 +transactions (including failed ones).  For example, see
     1.9 +src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency
    1.10 +output of transactions resulting in a new theory state.
    1.11 +
    1.12  * Name bindings in higher specification mechanisms (notably
    1.13  LocalTheory.define, LocalTheory.note, and derived packages) are now
    1.14  formalized as type Name.binding, replacing old bstring.