diff -r bb8ff5614ba7 -r d17f447fec02 ANNOUNCE
--- a/ANNOUNCE	Sat Nov 28 16:16:17 2009 +0100
+++ b/ANNOUNCE	Sat Nov 28 17:59:02 2009 +0100
@@ -26,11 +26,16 @@
 
 * HOL: various parts of multivariate analysis.
 
+* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
+arithmetic, based on external semidefinite programming solvers.
+
 * HOLCF: new definitional domain package.
 
 * Revised tutorial on locales.
 
-* Support for Poly/ML 5.3.0, with improved reporting of compiler
+* ML: tacticals for subgoal focus.
+
+* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
 errors and run-time exceptions, including detailed source positions.
 
 * Parallel checking of nested Isar proofs, with improved scalability