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 perfectlyIt'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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev