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