NEWS
changeset 45703 c7a13ce60161
parent 45625 750c5a47400b
child 45706 418846ea4f99
equal deleted inserted replaced
45702:7df60d1aa988 45703:c7a13ce60161
    20 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
    20 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
    21 declaration, and results are standardized before being stored.  Thus
    21 declaration, and results are standardized before being stored.  Thus
    22 old-style "standard" after instantiation or composition of facts
    22 old-style "standard" after instantiation or composition of facts
    23 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    23 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    24 indices of schematic variables.
    24 indices of schematic variables.
       
    25 
       
    26 * Renamed inner syntax categories "num" to "num_token" and "xnum" to
       
    27 "xnum_token", in accordance to existing "float_token".  Minor
       
    28 INCOMPATIBILITY.  Note that in practice "num_const" etc. are mainly
       
    29 used instead.
    25 
    30 
    26 
    31 
    27 *** Pure ***
    32 *** Pure ***
    28 
    33 
    29 * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    34 * Obsolete command 'types' has been discontinued.  Use 'type_synonym'