[isabelle-dev] Complete Distributive Lattice

Viorel Preoteasa viorel.preoteasa at aalto.fi
Mon Aug 28 20:26:27 CEST 2017

OK, I understand, what is the time frame for going back to normal? I did 
spent some time on this and I would like to see it finished.

As I mentioned earlier, I added finite lattices to simplify the proofs
in Enum.thy that finite_n are distributive complete lattices. However,
searching for dependencies on complete_distrib_lattice, I found a very 
similar class of finite lattices in Library. How should this be handled?


On 8/28/2017 5:26 PM, Lawrence Paulson wrote:
> For sure. The work is very welcome, but too drastic to undertake at this 
> precise moment.
> Larry
>> On 28 Aug 2017, at 13:08, Makarius <makarius at sketis.net 
>> <mailto:makarius at sketis.net>> wrote:
>> Nothing of this is relevant for the Isabelle2017 release. When the "RC"
>> versions show up, it is time to finish and not to start new things.

More information about the isabelle-dev mailing list