[isabelle] provers used by sledgehammer



Dear all,

how does sledgehammer decide which provers to use by default? After installing yices, I can do

  sledgehammer [yices]

to explicitly call yices. However, when using

  sledgehammer

it seems that "just" spass, e, remote_vampire, remote_e_sine, and z3 are run; but not yices. Can I change this globally (e.g., in my etc/settings) without having to use sledgehammer_params or explicitly setting options when calling sledgehammer?

cheers

chris





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