[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


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?



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