[isabelle-dev] NEWS

[Johannes Hölzl]

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