NEWS: new proof method "argo"
authorboehmes
Thu Sep 29 20:54:45 2016 +0200 (2016-09-29)
changeset 63963ed98a055b9a5
parent 63962 83a625d06e91
child 63964 9f0308e80366
NEWS: new proof method "argo"
NEWS
     1.1 --- a/NEWS	Thu Sep 29 20:54:45 2016 +0200
     1.2 +++ b/NEWS	Thu Sep 29 20:54:45 2016 +0200
     1.3 @@ -240,6 +240,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "argo" using the built-in Argo solver based on SMT technology.
     1.8 +The method can be used to prove goals of quantifier-free propositional logic,
     1.9 +goals based on a combination of quantifier-free propositional logic with equality,
    1.10 +and goals based on a combination of quantifier-free propositional logic with
    1.11 +linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for
    1.12 +examples.
    1.13 +
    1.14  * Type class "div" with operation "mod" renamed to type class "modulo" with
    1.15  operation "modulo", analogously to type class "divide".  This eliminates the
    1.16  need to qualify any of those names in the presence of infix "mod" syntax.