Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]



2013-10-04 15:13 Makarius:
> The sledgehammer manual then has this:
>
>   For Isabelle/jEdit users, Sledgehammer provides an automatic mode that
>   can be enabled via the “Auto Sledgehammer” option under “Plugins > Plugin
>   Options > Isabelle > General.” In this mode, Sledgehammer is run on
>   every newly entered theorem.
>
> The Plugin Options have more "automatically tried tools" in store, most
> of them off by default.

Thanks for pointing out!  Very interesting to know, but (now take this
as feedback from a naive end-user) I probably won't enable all these
automations seems.  Auto quickcheck and solve_direct are very nice, but
I wouldn't want time-consuming tools (such as Sledgehammer) to run
automatically even while I am still editing a statement.  I made it into
a habit to invoke "try" whenever I've finished writing down a statement.

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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