# HG changeset patch
# User nipkow
# Date 1255882084 -7200
# Node ID 078c1f7fa8beb0f97f299c6fbfa1ddc4810050ec
# Parent  b6ba8adc14c270a1c17b94003eb10c70f76b5d7c# Parent  2318ff5fca1afc0ac0026413ce469bf8a6e98bcf
merged

diff -r b6ba8adc14c2 -r 078c1f7fa8be NEWS
--- a/NEWS	Sun Oct 18 16:25:59 2009 +0200
+++ b/NEWS	Sun Oct 18 18:08:04 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