Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]
On Fri, 4 Oct 2013, Christoph LANGE wrote:
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.
The NEWS file has this very terse entry:
* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.
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.
"Auto methods" is the same mechanism as 'try0', but it tends to suck up a
lot of CPU resources, since the classic Isabelle proof tools easily get
into non-terminating situations without instrumentation by facts that are
properly classified as simp/intro/elim/dest/iff.
I should probably say a few more general things about the "auto" tools in
the still empty slots of the jedit manual, pointing to the other manuals,
We also need more practical experience with such options.
This archive was generated by a fusion of
Pipermail (Mailman edition) and