Am Mittwoch, den 24.04.2013, 11:45 +0200 schrieb Tjark Weber: > 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.
Thanks for noticing this! I changed it now in Isabelle #9328c6681f3c . I also renamed the type class linear_continuum_topology to connected_linorder_topology as they are not compact spaces. If somebody knows a better name for these spaces I'm also happy to rename them. - Johannes _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev