theory loader actions;
authorwenzelm
Mon, 09 Aug 1999 20:53:06 +0200
changeset 7196c8d1002060e8
parent 7195 a38dc0c6b244
child 7197 3ddf4a55d765
theory loader actions;
NEWS
     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)