* Generic Toplevel.add_hook interface allows to analyze the result of
transactions (including failed ones). For example, see
src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency
output of transactions resulting in a new theory state.

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