Re: [isabelle] nonterminating simp terminates without output
a student in our Isabelle-course has alerted me about the following behavior in Isabelle2017-RC2. (I'm currently traveling and can't test RC3.)
lemma [simp]: "length xs = length (rev xs)"
lemma "P (length xs)"
The second call to simp will turn from purple to red after a few minutes on my (and the student's) machine without outputting anything. In Isabelle2016-1, I couldn't reproduce this behavior (i.e., it would stay purple). The fact that it turns red is at least better than what happened in Isabelle2013-1, but it still can be confusing. Is this happening on purpose?
> On 23 Sep 2017, at 15:52, Makarius <makarius at sketis.net> wrote:
> Dear Isabelle users,
> the coming Isabelle2017 release is scheduled for the second week of
> October 2017. Thus there is still some time left for testing of release
> candidates, presently http://isabelle.in.tum.de/website-Isabelle2017-RC3
> Everything should be now ready and complete, including the "system" and
> "jedit" manuals.
> The corresponding repository versions of Isabelle and AFP are
> See also http://sketis.net/2017/release-candidates-for-isabelle2017 for
> notable changes within the line of release candidate.
> When posting problems, observations, suggestions, etc. the mail
> subject line should be changed to something meaningful, and the
> particular Isabelle version given in the message body.
This archive was generated by a fusion of
Pipermail (Mailman edition) and