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