[isabelle-dev] [isabelle] Good name for "sublist" predicates
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.
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev