merged
authornipkow
Sun, 18 Oct 2009 18:08:04 +0200
changeset 32993 078c1f7fa8be
parent 32991 b6ba8adc14c2 (current diff)
parent 32992 2318ff5fca1a (diff)
child 32994 ccc07fbbfefd
merged
--- 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