NEWS
changeset 32270 615c524bd9e4
parent 32264 0be31453f698
child 32326 9d70ecf11b7a
equal deleted inserted replaced
32269:b642e4813e53 32270:615c524bd9e4
    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 * New proof method "sos" (sum of squares) for nonlinear real arithmetic
       
    22 (originally due to John Harison). It requires Library/Sum_Of_Squares.
       
    23 It is not a complete decision procedure but works well in practice
       
    24 on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
       
    25 i.e. boolean combinations of equalities and inequalities between
       
    26 polynomials. It makes use of external semidefinite programming solvers.
       
    27 For more information and examples see Library/Sum_Of_Squares.
    20 
    28 
    21 * Set.UNIV and Set.empty are mere abbreviations for top and bot.  INCOMPATIBILITY.
    29 * Set.UNIV and Set.empty are mere abbreviations for top and bot.  INCOMPATIBILITY.
    22 
    30 
    23 * More convenient names for set intersection and union.  INCOMPATIBILITY:
    31 * More convenient names for set intersection and union.  INCOMPATIBILITY:
    24 
    32