[isabelle-dev] [isabelle] the sound of a sledgehammer
makarius at sketis.net
Fri Feb 15 14:19:46 CET 2013
On Fri, 15 Feb 2013, Tobias Nipkow wrote:
> Am 15/02/2013 13:12, schrieb Makarius:
>> * Sledgehammer has some kind of "home panel" which gives an overview of
>> results and some global controls.
> Triggering s/h via "sorry" (or some other explicit means) is perfectly
> reasonable, but having the IDE invoke s/h based on time outs and guesses
> should be avoided: the success rate is low and it consumes a lot of
> This is in contrast to auto-solve and quickcheck, both of which have a low
> overhead. Conceivably one could configure a s/h-very-light, which would be
> launched spontaneously.
So that is one of the "controls", to tell if it acts spontaneously or by
pushing a button in the panel. Heavy gear like Sledgehammer can be
non-spontaneous by default.
More information about the isabelle-dev