Sounds good to me. Can anybody think of an objection? Larry > On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev