[isabelle-dev] NEWS: new proof method "argo"

[Sascha Boehme]

*** 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.

This refers e.g. to Isabelle/ed98a055b9a5.