NEWS
changeset 50772 6973b3f41334
parent 50731 72624ff45676
child 50778 15dc91cf4750
     1.1 --- a/NEWS	Tue Jan 08 16:01:07 2013 +0100
     1.2 +++ b/NEWS	Tue Jan 08 16:23:07 2013 +0100
     1.3 @@ -38,6 +38,13 @@
     1.4  specifications: nesting of "context fixes ... context assumes ..."
     1.5  and "class ... context ...".
     1.6  
     1.7 +* Attribute "consumes" allows a negative value as well, which is
     1.8 +interpreted relatively to the total number if premises of the rule in
     1.9 +the target context.  This form of declaration is stable when exported
    1.10 +from a nested 'context' with additional assumptions.  It is the
    1.11 +preferred form for definitional packages, notably cases/rules produced
    1.12 +in HOL/inductive and HOL/function.
    1.13 +
    1.14  * More informative error messages for Isar proof commands involving
    1.15  lazy enumerations (method applications etc.).
    1.16