webertj at in.tum.de
Wed Apr 24 11:45:36 CEST 2013
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.
More information about the isabelle-dev