Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem

Put YICES_INSTALLED="yes" in your "~/Isabelle2012/etc/settings" file,
and yices will be one of the available solvers when you use the command
"sledgehammer supported_provers" under a theorem. The pertinent thread
is "sledgehammer / yices":

Just to clarify: YICES_INSTALLED="yes" alone won't work if the yices binary is not installed and set up correctly (as described in `isabelle doc sledgehammer`), since the standard Isabelle bundle does not include this binary due to licensing issues.



PS: Z3_NON_COMMERCIAL="yes" (in your etc/settings) is also a way to add an additional prover and works out of the box.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.