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 <l...@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.preote...@gmail.com> < > viorel.preote...@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? > > > >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
