[isabelle-dev] Complete Distributive Lattice

viorel.preoteasa at gmail.com viorel.preoteasa at gmail.com
Thu Mar 8 22:35:54 CET 2018

I am working on the generalization of the complete distributive lattices. Changing the axioms from


sup  x (Inf Y) = …


to the more general form:


Sup (Inf ` A) = …


I have done these changes already for the previous release candidate, and I just need to integrate them into the current repository version.

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?


Best regards,


Viorel Preoteasa



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180308/6793fc6c/attachment.html>

More information about the isabelle-dev mailing list