NEWS
changeset 57946 6a26aa5fa65e
parent 57941 57200bdc2aa7
child 57983 6edc3529bb4e
child 58008 aa72531f972f
--- a/NEWS	Sat Aug 16 11:35:33 2014 +0200
+++ b/NEWS	Sat Aug 16 12:10:36 2014 +0200
@@ -9,6 +9,11 @@
 * Commands 'method_setup' and 'attribute_setup' now work within a
 local theory context.
 
+* Command 'named_theorems' declares a dynamic fact within the context,
+together with an attribute to maintain the content incrementally.
+This supersedes functor Named_Thms, but with a subtle change of
+semantics due to external visual order vs. internal reverse order.
+
 
 *** HOL ***