[isabelle-dev] Complete Distributive Lattice

Lawrence Paulson lp15 at cam.ac.uk
Fri Mar 9 11:48:43 CET 2018

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?

More information about the isabelle-dev mailing list