NEWS
changeset 50772 6973b3f41334
parent 50731 72624ff45676
child 50778 15dc91cf4750
equal deleted inserted replaced
50771:2852f997bfb5 50772:6973b3f41334
    35 remaining material in old "ref" manual.
    35 remaining material in old "ref" manual.
    36 
    36 
    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 
       
    41 * Attribute "consumes" allows a negative value as well, which is
       
    42 interpreted relatively to the total number if premises of the rule in
       
    43 the target context.  This form of declaration is stable when exported
       
    44 from a nested 'context' with additional assumptions.  It is the
       
    45 preferred form for definitional packages, notably cases/rules produced
       
    46 in HOL/inductive and HOL/function.
    40 
    47 
    41 * More informative error messages for Isar proof commands involving
    48 * More informative error messages for Isar proof commands involving
    42 lazy enumerations (method applications etc.).
    49 lazy enumerations (method applications etc.).
    43 
    50 
    44 * Refined 'help' command to retrieve outer syntax commands according
    51 * Refined 'help' command to retrieve outer syntax commands according