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

Tobias Nipkow nipkow at in.tum.de
Fri Jun 30 16:23:34 CEST 2017

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.


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>

More information about the isabelle-dev mailing list