nipkow at in.tum.de
Mon Sep 2 14:01:33 CEST 2013
Am 02/09/2013 13:13, schrieb 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.
If you take asynhronous processing seriously you shouldn't have to wait until
the end before you make your choice but you should be able to revert your
decision if something better comes up. In such cases the user should be
responsibe for removing the first proof. But you are right, this could lead to
complications in the implementation.
> I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings.
> 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
>> - 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.
More information about the isabelle-dev