--- 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.