# HG changeset patch
# User wenzelm
# Date 1220388096 -7200
# Node ID fb16a07d6580f215dda0454f7ba7aa9ebd47fb88
# Parent  c92850d2d16cdba65de28b57e68250274501d740
* 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.

diff -r c92850d2d16c -r fb16a07d6580 NEWS
--- 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.