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

[Sebastien Gouezel]

Le 30/06/2017 à 20:41, Manuel Eberl a écrit :

> 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.

strict_mono would be perfectly OK if there is a comment in the library 
around there mentioning subsequences, that could be found by grepping 
the library (I found out that grepping the library or the AFP for 
mathematical keywords is often the most efficient way to locate facts or 
definitions related to a given concept).

> It's "Topological_Spaces.compact" and that should definitely work.

Yes, it works. Strangely, topological_space.compact is recognized as 
valid syntax (contrary, say, to metric_space.compact), that's why I 
didn't spot my mistake.

Thanks!
Sebastien