On 2017-06-30 20:33, Sebastien Gouezel wrote: > I used subseq quite heavily in my ergodic theory developments. From > a mathematician point of view, taking subsequences of sequences > from nat to nat is very common and very useful in analysis (much > more than taking subsequences of lists).
So what about the suggestion of just writing "strict_mono" instead? Besides, you can always introduce local abbreviations for things with "notation" and delete them with "no_notation" afterwards. > 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. Cheers, Manuel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
