Dear Makarius,
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?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
