<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Sounds good to me. Can anybody think of an objection?<br class=""><div class="">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; border-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-stroke-width: 0px;"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Larry</div></div></span>
</div>
<br class=""><div style=""><blockquote type="cite" class=""><div class="">On 23 Aug 2017, at 15:17, Viorel Preoteasa <<a href="mailto:viorel.preoteasa@aalto.fi" class="">viorel.preoteasa@aalto.fi</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hello,<br class=""><br class="">I am not sure if this is the right place to post this message, but it is<br class="">related to the upcoming release as I am prosing adding something<br class="">to the Isabelle library.<br class=""><br class="">While working with complete distributive lattices, I noticed that<br class="">the Isabelle class complete_distrib_lattice is weaker compared to<br class="">what it seems to be regarded as a complete distributive lattice.<br class=""><br class="">As I needed the more general concept, I have developed it,<br class="">and if Isabelle community finds it useful to be in the library,<br class="">then I could provide the proofs or integrate it myself in the<br class="">Complete_Lattice.thy<br class=""><br class="">The only axiom needed for complete distributive lattices is:<br class=""><br class="">Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"<br class=""><br class="">and from this, the equality and its dual can be proved, as well as<br class="">the existing axioms of complete_distrib_lattice and the instantiation<br class="">to bool, set and fun.<br class=""><br class="">Best regards,<br class=""><br class="">Viorel<br class=""><br class=""><br class="">On 2017-08-21 21:24, Makarius wrote:<br class=""><blockquote type="cite" class="">Dear Isabelle contributors,<br class=""><br class="">we are now definitely heading towards the Isabelle2017 release.<br class=""><br class="">The first official release candidate Isabelle2017-RC1 is anticipated for<br class="">2/3-Sep-2017, that is a bit less than 2 weeks from now.<br class=""><br class="">That is also the deadline for any significant additions.<br class=""><br class=""><br class="">I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE<br class="">in Isabelle/5c0a3f63057d, but it seems that many potential entries are<br class="">still missing.<br class=""><br class="">Please provide entries in NEWS and CONTRIBUTORS for all relevant things<br class="">you have done since the last release.<br class=""><br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></div></blockquote></div><br class=""></body></html>