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?


	Makarius





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