*** 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
