[isabelle-dev] linear_continuum_topology (was: NEWS)

Johannes Hölzl hoelzl at in.tum.de
Thu Apr 25 12:03:09 CEST 2013

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

More information about the isabelle-dev mailing list