On Wed, 18 Apr 2012, Christian Sternagel wrote:
it's very nice that after sledgehammer found a proof command to finish a
proof, I can simply click on this command in the output buffer to
include it in the main buffer! A slight oddity is that this merges
lines. E.g.,
lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
sledgehammer
end
After sledgehammer reports
"remote_e": Try this: by (metis append_eq_conv_conj) (21 ms).
In the output buffer. I click on "by (metis append_eq_conv_conj)" and
the result is.
lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
by (metis append_eq_conv_conj)end
Maybe this could be changed such that "end" stays on its own line?
I've destroyed this recently when changing the meaning of a command span,
to include its trailing white spans, which miraculously cuts the total
number of command transactions in half and thus improves editing
performance.
In Isabelle/26d0a76fef0a it should work again. I've made further
refinements here and in Isabelle/9980c0c094b8
So even without the long anticipated integration of "asynchronous agents"
into the Isabelle/jEdit document model, which I had to cancel again for
this release to take place, sledgehammer should work reasonably well.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
