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