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

[Florian Haftmann]

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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170701/3a16f67c/attachment-0001.asc>