*To*: Makarius <makarius at sketis.net>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle2016-1-RC0 available for testing*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 26 Oct 2016 08:58:49 +0200*In-reply-to*: <51aeb3e5-4a86-e7e8-68d3-fa3d782847e7@sketis.net>*References*: <5e6dd458-abf5-f814-3699-f941873ba942@sketis.net> <d0ee5524-27d3-9567-104e-3839d887628c@inf.ethz.ch> <51aeb3e5-4a86-e7e8-68d3-fa3d782847e7@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Hi Makarius,

Best, Andreas 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

**Attachment:
Scratch.thy**

**References**:**[isabelle] Isabelle2016-1-RC0 available for testing***From:*Makarius

**Re: [isabelle] Isabelle2016-1-RC0 available for testing***From:*Andreas Lochbihler

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

- Previous by Date: Re: [isabelle] Eisbach matching with schematic variables
- Next by Date: Re: [isabelle] Isabelle2016-RC0: cvc4 crashing
- Previous by Thread: Re: [isabelle] Isabelle2016-1-RC0 available for testing
- Next by Thread: Re: [isabelle] Isabelle2016-1-RC0 available for testing
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list