Johannes, On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote: > * Introduce type class "conditional_complete_lattice": Like a complete > lattice but does not assume the existence of the top and bottom elements.
The name "conditional complete lattice" suggests a special kind of complete lattice. However, without top and bottom elements, this structure is not a complete lattice at all. In the literature, it is therefore more aptly called "conditionally complete lattice." I propose to retain the "-ly" suffix in the name of the type class. Best, Tjark _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
