--- a/NEWS Tue Jan 08 16:01:07 2013 +0100
+++ b/NEWS Tue Jan 08 16:23:07 2013 +0100
@@ -38,6 +38,13 @@
specifications: nesting of "context fixes ... context assumes ..."
and "class ... context ...".
+* Attribute "consumes" allows a negative value as well, which is
+interpreted relatively to the total number if premises of the rule in
+the target context. This form of declaration is stable when exported
+from a nested 'context' with additional assumptions. It is the
+preferred form for definitional packages, notably cases/rules produced
+in HOL/inductive and HOL/function.
+
* More informative error messages for Isar proof commands involving
lazy enumerations (method applications etc.).