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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
