Hi all,

Yes, it absolutely makes sense to change the situation with compact. It is a standard notion in order theory, so my suggestion is to make it qualified with ccpo, just like admissible and fixp are. I can take care of that.


Andreas

On 30/06/17 21:31, Tobias Nipkow wrote:

On 30/06/2017 20:41, Manuel Eberl wrote:
By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly
It's "Topological_Spaces.compact" and that should definitely work. We
should probably make the one from Complete_Partial_Order2 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.

Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or renaming that "compact" in the most appropriate way.

Tobias



_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to