Re: [isabelle] Isabelle2013-1-RC4 available for testing
After I've run Sledgehammer once in the panel by clicking "Apply", it
will run on its own, and here is the description:
The following is in the file Scratch.thy, in a new Cygwin installation
in which I've changed no options.
theorem "A = A"
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.
So, I can edit anything after "A = A", but if I make any edits before
"theorem", it runs on its own, even if I click on a proof so that it's
inserted. This happens every time after I exit and restart jEdit, and
there are no other files open.
There's also no persistence in the "Provers" field. The "Previously
entered strings" is always empty, no matter how many times I've edited
the field. I don't care about that. I'm just reporting it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and