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

[Tobias Nipkow]

In theory that solves the problem, but the point is that 
Topological_Spaces.subseq is impractical for a frequently used symbol. It would 
be nice if non-quaified names could be found for this case.

Tobias

On 30/06/2017 16:14, Lawrence Paulson wrote:
> Indeed we do.
> Larry
> 
>> On 28 Jun 2017, at 18:49, Manuel Eberl <eberlm at in.tum.de 
>> <mailto:eberlm at in.tum.de>> wrote:
>>
>> Yes, I noticed that as well. I decided to leave it that way since, well,
>> we do have qualified names.
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/8978de7c/attachment.bin>