# HG changeset patch
# User wenzelm
# Date 934224786 -7200
# Node ID c8d1002060e89372228960cfa507e8613aba7304
# Parent  a38dc0c6b2447a23821fd95bc0f8bf09acc8ef47
theory loader actions;

diff -r a38dc0c6b244 -r c8d1002060e8 NEWS
--- a/NEWS	Fri Aug 06 22:43:51 1999 +0200
+++ b/NEWS	Mon Aug 09 20:53:06 1999 +0200
@@ -196,6 +196,11 @@
 * refined token_translation interface; INCOMPATIBILITY: output length
 now of type real instead of int;
 
+* theory loader actions may be traced via new ThyInfo.add_hook
+interface (see src/Pure/Thy/thy_info.ML); example application: keep
+your own database of information attached to *whole* theories -- as
+opposed to intra-theory data slots offered via TheoryDataFun;
+
 
 
 New in Isabelle98-1 (October 1998)