Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have



Dear Makarius,

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?

Also

  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?

cheers

chris

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
> http://sketis.net/2016/release-candidates-for-isabelle2016-1.
> 
> 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
> https://bitbucket.org/isabelle_project/isabelle-release/commits/8bf3d0553c35
> 
> 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.
> 
> 
> 	Makarius
> 




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