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.
isabelle-dev mailing list