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



isabelle-dev mailing list

Reply via email to