Re: [isabelle] Isabelle2013-1-RC4 available for testing
On Sun, 10 Nov 2013, Gottfried Barrow wrote:
After I've run Sledgehammer once in the panel by clicking "Apply", it will
run on its own, and here is the description:
I place my cursor after "A = A", I click "Apply", Sledgehammer runs, and it
returns "Try this: by metis (1 ms)" for e, spass, remote_vampire, and that I
need to change "Z3_NON_COMMERCIAL" to yes.
I place my cursor at the empty line before "theorem", hit the space bar,
Sledgehammer runs again on its own, returns the same results, and it
terminates like it should.
That is an interesting corollary of sledgehammer as "query operation".
The sledgehammer invocation is associated with a "document overlay", based
on the static command 'theorem', and it remains there until you invoke it
differently. So when you edit before that command, it is re-checked
together with its sledgehammer overlay.
This gives the effect of "run on its own". The "Cancel" button is not
sufficient to remove the potential sledgehammer run, it only refers to the
current dynamic execution of it. So to dispose sledgehammer permanently,
you need to apply it elsewhere (e.g. outside a proof context), or undock
There's also no persistence in the "Provers" field.
The persistence is in the history of the text field. This is also useful
to "park" several sets of options that are commonly used.
This archive was generated by a fusion of
Pipermail (Mailman edition) and