Re: [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  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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

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