[isabelle] Fwd: Re: provers used by sledgehammer



Let me reformulate ;). Why not use all installed provers by default? (If I wouldn't want to use it I would hardly install a prover.)
-cheers chris

On 07/20/2012 04:19 PM, Jasmin Blanchette wrote:
Am 20.07.2012 um 04:46 schrieb Christian Sternagel:

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?

If you change it through the good old Proof General settings, I think it will do the right thing and remember it across sessions. Otherwise, no: That's what "sledgehammer_params" is for, and it would be tedious to emulate its functionality in "etc/settings" (e.g. to change the default timeout or whatever else...).

Cheers,

Jasmin








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