Re: [isabelle] Sledgehammer settings

On Mon, 11 Nov 2013, Gottfried Barrow wrote:

On 11/11/2013 4:52 AM, Makarius wrote:
Invoking sledgehammer by hand introduces an extra dimension of complication. What are the remaining reasons to do so?

To be able to change the default options.

That is not inherent in the separate command vs. panel. It is merely accidental which options are available where.

At some point I need to discuss with Jasmin to sort out what really needs to be supported in the panel, such that a manual invocation of the sledgehammer command becomes a rare event.


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