Re: [isabelle] Isabelle2016-1-RC0 available for testing

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.