[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

-- 
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.