[isabelle-dev] linear_continuum_topology (was: NEWS)
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.
More information about the isabelle-dev