Re: [isabelle] Isabelle2016-1-RC0 available for testing
Yes, that was me. The "transfer" tool is the most "reliable" way to
produce such a situation, but I occasionally observe similar situations
with other proof methods as well.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and