[isabelle] Fwd: Re: provers used by sledgehammer
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Fwd: Re: provers used by sledgehammer
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Fri, 20 Jul 2012 16:45:25 +0900
- In-reply-to: <500908B5.firstname.lastname@example.org>
- References: <500908B5.email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120615 Thunderbird/13.0.1
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.)
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...).
This archive was generated by a fusion of
Pipermail (Mailman edition) and