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