[isabelle-dev] [isabelle] Good name for "sublist" predicates

[Manuel Eberl]

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