NEWS
changeset 45233 28b076e0bea8
parent 45210 b416573f1807
child 45293 57def0b39696
equal deleted inserted replaced
45232:eb56e1774c26 45233:28b076e0bea8
    10 instead.  INCOMPATIBILITY.
    10 instead.  INCOMPATIBILITY.
    11 
    11 
    12 * Ancient code generator for SML and its commands 'code_module',
    12 * Ancient code generator for SML and its commands 'code_module',
    13  'code_library', 'consts_code', 'types_code' have been discontinued.
    13  'code_library', 'consts_code', 'types_code' have been discontinued.
    14   Use commands of the generic code generator instead. INCOMPATIBILITY.
    14   Use commands of the generic code generator instead. INCOMPATIBILITY.
       
    15 
       
    16 * Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
       
    17 instead. INCOMPATIBILITY.
    15 
    18 
    16 *** HOL ***
    19 *** HOL ***
    17 
    20 
    18 * 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
    21 * 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
    19 
    22