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

[Tobias Nipkow]

On 30/06/2017 20:41, Manuel Eberl wrote:
>> 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.

Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or 
renaming that "compact" in the most appropriate way.

Tobias

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170630/c596fb43/attachment.bin>