Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.
If anybody has better suggestions, I am open to implementing them.
Manuel
On 2017-06-28 17:05, Andreas Lochbihler wrote:
> Dear all,
>
> While porting some of my theories to the current
Dear all,
While porting some of my theories to the current development version, I've just noticed
that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad
effect:
The name subseq is already used in Topological_Spaces to formalise the concept of a
