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

Sebastien Gouezel sebastien.gouezel at univ-nantes.fr
Fri Jun 30 20:55:38 CEST 2017


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




More information about the isabelle-dev mailing list