1.1 --- a/ANNOUNCE	Sat Nov 28 16:16:17 2009 +0100
     1.2 +++ b/ANNOUNCE	Sat Nov 28 17:59:02 2009 +0100
     1.3 @@ -26,11 +26,16 @@
     1.4  
     1.5  * HOL: various parts of multivariate analysis.
     1.6  
     1.7 +* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
     1.8 +arithmetic, based on external semidefinite programming solvers.
     1.9 +
    1.10  * HOLCF: new definitional domain package.
    1.11  
    1.12  * Revised tutorial on locales.
    1.13  
    1.14 -* Support for Poly/ML 5.3.0, with improved reporting of compiler
    1.15 +* ML: tacticals for subgoal focus.
    1.16 +
    1.17 +* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
    1.18  errors and run-time exceptions, including detailed source positions.
    1.19  
    1.20  * Parallel checking of nested Isar proofs, with improved scalability