hoelzl at in.tum.de
Thu Apr 25 10:56:32 CEST 2013
Am Mittwoch, den 24.04.2013, 11:45 +0200 schrieb Tjark Weber:
> 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.
More information about the isabelle-dev