Just for the record: * Topological_Spaces.subseq has already been present before 2007 in HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7)
* strict_mono has entered in 2009, see abefe1dfadbb Hence we have the typical situation that a generalized constant subsumes a more ancient unconsciously. Cheers, Florian Am 30.06.2017 um 20:41 schrieb 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 > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev