Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]
2013-10-07 12:25 Jasmin Blanchette:
> 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.
OK, thanks, you convinced me. I'll give Auto Sledgehammer a try. And
otherwise fall back to "try" if I don't like it.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and