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?
isabelle-dev mailing list