Hi Makarius,All the concrete cases in which I ran into this problem have been fixed now. But I've attached a small example that shows the problem. The lemma has a pointless assumption, but this is only to get the theorem sufficiently large such that transfer runs for a while
As is, the proof of the lemma goes through, but if you delete the declaration of map_concat as a simp rule, then it will not, but keep running for quite some time (if your patience is longer than mine, just add a few more universal quantifiers in the assumptions of the lemma; the backtracking in transfer grows exponentially with the number of quantifiers). What I then typically do is to change the non-terminating line of proof, usually by adding a space somewhere in transfer (i.e., "by tra nsfer simp") or completely deleting it.
But despite these changes, the proof method keeps running and Isabelle/jEdit does no longer update the Output and State panels any more.
Best, Andreas On 25/10/16 14:15, Makarius wrote:
On 10/10/16 17:07, Andreas Lochbihler wrote:I played a bit with RC0 and noticed that reactivity seems to be a bit lower than with Isabelle2016. In particular, when I have a non-terminating proof command like subgoal by transfer simp and (due to some changes in the theory above) the proof loops, then I have found no way to interrupt the proof.Someone else reported a similar problem some weeks ago. Is there a concrete example somewhere, that shows the effect? Makarius