# HG changeset patch
# User nipkow
# Date 1255882064 -7200
# Node ID 2318ff5fca1afc0ac0026413ce469bf8a6e98bcf
# Parent  c28279b29ff1c71819f94ff1c1517138b88ac2cb
certificates for sos

diff -r c28279b29ff1 -r 2318ff5fca1a NEWS
--- a/NEWS	Sun Oct 18 12:07:56 2009 +0200
+++ b/NEWS	Sun Oct 18 18:07:44 2009 +0200
@@ -82,8 +82,10 @@
 works well in practice on quantifier-free real arithmetic with +, -,
 *, ^, =, <= and <, i.e. boolean combinations of equalities and
 inequalities between polynomials. It makes use of external
-semidefinite programming solvers.  For more information and examples
-see src/HOL/Library/Sum_Of_Squares.
+semidefinite programming solvers. Method "sos" generates a certificate
+that can be pasted into the proof thus avoiding the need to call an external
+tool every time the proof is checked.
+For more information and examples see src/HOL/Library/Sum_Of_Squares.
 
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold