Re: [isabelle] Sledgehammer settings



Hi,

Am Montag, den 11.11.2013, 11:52 +0100 schrieb Makarius:
> On Fri, 8 Nov 2013, Jasmin Blanchette wrote:
> > Am 08.11.2013 um 11:10 schrieb Joachim Breitner <breitner at kit.edu>:
> >
> >> I noticed that the sledgehammer timeout can be configured in the 
> >> Isabelle plugin settings of jEdit. I would appreciate if I could also 
> >> configure the set of default solvers there, so that it would apply to 
> >> both “sledgehammer” entered by hand, and the sledgehammer panel.
> 
> Invoking sledgehammer by hand introduces an extra dimension of 
> complication.  What are the remaining reasons to do so?

 * not having to touch the mouse,
 * changing a now failing 
       by (metis a b c d e )
   to
       sledgehammer (add: a b c d e)
   which is often faster running sledgehammer without hints
 * visual feedback in the document about where sledgehammer is running 
   (as far as I could tell, the sledgehammer panel does not leave a 
   mark in the document, e.g. a spinner of some kind, which would be 
   useful visual feedback).
 * and of course: habit ;-)

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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