[isabelle-dev] sledgehammer

[Lawrence Paulson]

I have also noticed the first issue you mention.

Regarding your other points, a) seems logical to me (you have made your choice), while b) possibly simplifies the implementation significantly (otherwise you need to remember to replace the previous choice rather than to append the text), and it is only necessary in the fairly unusual case where your first choice simply didn't work.

I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings.

Larry

On 2 Sep 2013, at 11:31, Tobias Nipkow <nipkow at in.tum.de> wrote:

> - Sometimes I click on the generated proof and it is not pasted into the theory
> text. It just doesn't work, even if I click repeatedly.  I cannot reproduce this
> reliably.
> 
> - Once one has clicked on a proposed proof and it has been pasted into the
> theory window, this does two things:
>  a) it stops the rest of the running atps.
>  b) it disables all the proposed proofs, i.e. no more click-and-paste for any
> of them.
> Neither is desirable and I thought at least a) was not the case in the past.