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.

Manuel


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
> 
> 




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