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 ***