Sounds good to me. Can anybody think of an objection?
Larry
> On 23 Aug 2017, at 15:17, Viorel Preoteasa 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