ANNOUNCE
changeset 33914 d17f447fec02
parent 33881 d8958955ecb5
child 37159 07f3f5a03e98
equal deleted inserted replaced
33913:bb8ff5614ba7 33914:d17f447fec02
    24 
    24 
    25 * HOL: refined number theory.
    25 * HOL: refined number theory.
    26 
    26 
    27 * HOL: various parts of multivariate analysis.
    27 * HOL: various parts of multivariate analysis.
    28 
    28 
       
    29 * HOL-Library: proof method "sos" (sum of squares) for nonlinear real
       
    30 arithmetic, based on external semidefinite programming solvers.
       
    31 
    29 * HOLCF: new definitional domain package.
    32 * HOLCF: new definitional domain package.
    30 
    33 
    31 * Revised tutorial on locales.
    34 * Revised tutorial on locales.
    32 
    35 
    33 * Support for Poly/ML 5.3.0, with improved reporting of compiler
    36 * ML: tacticals for subgoal focus.
       
    37 
       
    38 * ML: support for Poly/ML 5.3.0, with improved reporting of compiler
    34 errors and run-time exceptions, including detailed source positions.
    39 errors and run-time exceptions, including detailed source positions.
    35 
    40 
    36 * Parallel checking of nested Isar proofs, with improved scalability
    41 * Parallel checking of nested Isar proofs, with improved scalability
    37 up to 8 cores.
    42 up to 8 cores.
    38 
    43