[isabelle-dev] Towards the Isabelle2017 release

[Lawrence Paulson]

Sounds good to me. Can anybody think of an objection?
Larry

> On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
> 
> Hello,
> 
> I am not sure if this is the right place to post this message, but it is
> related to  the upcoming release as I am prosing adding something
> to the Isabelle library.
> 
> While working with complete distributive lattices, I noticed that
> the Isabelle class complete_distrib_lattice is weaker compared to
> what it seems to be regarded as a complete distributive lattice.
> 
> As I needed the more general concept, I have developed it,
> and if Isabelle community finds it useful to be in the library,
> then I could provide the proofs or integrate it myself in the
> Complete_Lattice.thy
> 
> The only axiom needed for complete distributive lattices is:
> 
> Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"
> 
> and from this, the equality and its dual can be proved, as well as
> the existing axioms of complete_distrib_lattice and the instantiation
> to bool, set and fun.
> 
> Best regards,
> 
> Viorel
> 
> 
> On 2017-08-21 21:24, Makarius wrote:
>> Dear Isabelle contributors,
>> 
>> we are now definitely heading towards the Isabelle2017 release.
>> 
>> The first official release candidate Isabelle2017-RC1 is anticipated for
>> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>> 
>> That is also the deadline for any significant additions.
>> 
>> 
>> I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
>> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
>> still missing.
>> 
>> Please provide entries in NEWS and CONTRIBUTORS for all relevant things
>> you have done since the last release.
>> 
>> 
>> 	Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170823/80dcb136/attachment-0002.html>