NEWS
changeset 32134 ee143615019c
parent 32079 5dc52b199815
child 32136 672dfd59ff03
equal deleted inserted replaced
32133:b513db807fca 32134:ee143615019c
    15 * On instantiation of classes, remaining undefined class parameters
    15 * On instantiation of classes, remaining undefined class parameters
    16 are formally declared.  INCOMPATIBILITY.
    16 are formally declared.  INCOMPATIBILITY.
    17 
    17 
    18 
    18 
    19 *** HOL ***
    19 *** HOL ***
       
    20 
       
    21 * More convenient names for set intersection and union.  INCOMPATIBILITY:
       
    22 
       
    23     Set.Int ~>  Set.inter
       
    24     Set.Un ~>   Set.union
    20 
    25 
    21 * Code generator attributes follow the usual underscore convention:
    26 * Code generator attributes follow the usual underscore convention:
    22     code_unfold     replaces    code unfold
    27     code_unfold     replaces    code unfold
    23     code_post       replaces    code post
    28     code_post       replaces    code post
    24     etc.
    29     etc.