[isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

My changes to Complete Distributive Lattices are now integrated in the
development version of Isabelle.

I want to thank Manuel Eberl for helping with testing and pushing the
update into repository.

Viorel Preoteasa

On Fri, Mar 9, 2018 at 12:48 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I don’t think it’s a problem that your more general theorems require the
> Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from
> it).
>
> Larry Paulson
>
>
>
> > On 8 Mar 2018, at 21:35, <viorel.preoteasa at gmail.com> <
> viorel.preoteasa at gmail.com> wrote:
> >
> > I have a question about how to organize these changes. The problem is
> that most of the results for the more general lattice (instantiations
> > to set, fun) require Hilbert_Choice which is not available in
> Complete_Lattice. Now I have added all results about complete distributive
> > lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this
> acceptable?
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180314/09e9d560/attachment-0002.html>