Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]
> 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.
Auto Sledgehammer and Auto Nitpick run in a much reduced mode -- e.g. Sledgehammer just tries one prover for a few seconds instead of four for half a minute. (The manuals of these tools clarify which options are used.) I've enabled them months ago and don't really notice them any more than I notice Auto Quickcheck or Auto solve_direct. On the other hand, if you invoke "try" regularly, I can see that you don't need those tools.
This archive was generated by a fusion of
Pipermail (Mailman edition) and