[isabelle-dev] [isabelle] the sound of a sledgehammer

[Makarius]

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 
> resources.
>
> 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.


 	Makarius