Functor NamedThmsFun: data is available to the user as dynamic fact;
authorwenzelm
Tue Mar 25 22:12:02 2008 +0100 (2008-03-25)
changeset 26401e7a94081dce7
parent 26400 2f0500e375fe
child 26402 441ddf3b8f02
Functor NamedThmsFun: data is available to the user as dynamic fact;
NEWS
     1.1 --- a/NEWS	Tue Mar 25 21:59:48 2008 +0100
     1.2 +++ b/NEWS	Tue Mar 25 22:12:02 2008 +0100
     1.3 @@ -172,6 +172,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Functor NamedThmsFun: data is available to the user as dynamic fact
     1.8 +(of the same name).
     1.9 +
    1.10  * Removed obsolete "use_legacy_bindings" function.  INCOMPATIBILITY.
    1.11  
    1.12  * ML within Isar: antiquotation @{const name} or @{const