# HG changeset patch
# User boehmes
# Date 1475175285 -7200
# Node ID ed98a055b9a59608c9b46795023af7e2ba2fd222
# Parent  83a625d06e91ff94d5ea1d259782a709bf3cb71c
NEWS: new proof method "argo"

diff -r 83a625d06e91 -r ed98a055b9a5 NEWS
--- a/NEWS	Thu Sep 29 20:54:45 2016 +0200
+++ b/NEWS	Thu Sep 29 20:54:45 2016 +0200
@@ -240,6 +240,13 @@
 
 *** HOL ***
 
+* New proof method "argo" using the built-in Argo solver based on SMT technology.
+The method can be used to prove goals of quantifier-free propositional logic,
+goals based on a combination of quantifier-free propositional logic with equality,
+and goals based on a combination of quantifier-free propositional logic with
+linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for
+examples.
+
 * Type class "div" with operation "mod" renamed to type class "modulo" with
 operation "modulo", analogously to type class "divide".  This eliminates the
 need to qualify any of those names in the presence of infix "mod" syntax.