# HG changeset patch
# User wenzelm
# Date 1206479522 -3600
# Node ID e7a94081dce70376169f2bc46c01a9318ee15e04
# Parent  2f0500e375fe2267fbe2d19e83ec0ef7ab299dfd
Functor NamedThmsFun: data is available to the user as dynamic fact;

diff -r 2f0500e375fe -r e7a94081dce7 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