Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have
I use "moreover then have" a lot (mostly as the first "moreover"-step).
But in the RC "then" is highlighted in red, which tells me that I
shouldn't do this. Why?
moreover have "..." using 1
is okay, while in
from 1 moreover have "..."
'moreover' and 'have' are highlighted in red. Shouldn't both forms
essentially be the same?
On 11/22/2016 10:36 AM, Makarius wrote:
> Dear Isabelle users,
> after more than 2 weeks, here is the next release candidate for
> Isabelle2016-1 (December 2016):
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC3 -- see also
> More fine points have been consolidated. A component for the new
> experimental Nunchaku tool has been included.
> The corresponding repository versions of Isabelle and AFP are
> and https://bitbucket.org/isa-afp/afp-devel/commits/1a3901597f0f
> It is also possible to follow nightly development snapshots from
> http://isabelle.in.tum.de/devel although they might be somewhat erratic.
> At this stage, Isabelle release candidates are already sufficiently
> consolidated to be ready for everyday use. Adapting your applications
> now gives a unique chance for feedback before the release is finalized.
> When discussing problems, observations, suggestions, etc. the mail
> subject line should be changed to something informative, and the
> particular Isabelle version given in the message body.
This archive was generated by a fusion of
Pipermail (Mailman edition) and