NEWS
changeset 50778 15dc91cf4750
parent 50772 6973b3f41334
child 50836 c95af99e003b
equal deleted inserted replaced
50777:20126dd9772c 50778:15dc91cf4750
    37 * Improved support for auxiliary contexts indicate block structure for
    37 * Improved support for auxiliary contexts indicate block structure for
    38 specifications: nesting of "context fixes ... context assumes ..."
    38 specifications: nesting of "context fixes ... context assumes ..."
    39 and "class ... context ...".
    39 and "class ... context ...".
    40 
    40 
    41 * Attribute "consumes" allows a negative value as well, which is
    41 * Attribute "consumes" allows a negative value as well, which is
    42 interpreted relatively to the total number if premises of the rule in
    42 interpreted relatively to the total number of premises of the rule in
    43 the target context.  This form of declaration is stable when exported
    43 the target context.  This form of declaration is stable when exported
    44 from a nested 'context' with additional assumptions.  It is the
    44 from a nested 'context' with additional assumptions.  It is the
    45 preferred form for definitional packages, notably cases/rules produced
    45 preferred form for definitional packages, notably cases/rules produced
    46 in HOL/inductive and HOL/function.
    46 in HOL/inductive and HOL/function.
    47 
    47