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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev