[isabelle-dev] linear_continuum_topology (was: NEWS)

[Johannes Hölzl]

Am Donnerstag, den 25.04.2013, 10:56 +0200 schrieb Johannes Hölzl:
> 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. 

Okay, forget this.

"linear_continuum_topology" is actually the right name. But we need the
additional axiom that the type has more than one element.


  - Johannes