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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
