[isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]
2013-10-04 10:42 Makarius:
> With the implicit "auto sledgehammer" and explicit "slegdehammer panel"
> you normally don't put query commands in the buffer anymore,
Could you once more explain what "auto sledgehammer" is? I know
entering "sledgehammer" (or "try", which I use in practice most of the
time) into the buffer, and I know the new sledgehammer panel, and I
didn't see anything else in the NEWS file.
Cheers, and thanks in advance,
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