Re: [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 <ebe...@in.tum.de <mailto:ebe...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev