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 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 subsequence. This name is now hidden by the definition in > Sublist, in particular when I import HOL-Probability. > > Can this name clash be eliminated before the next release such that I > don't have to write Topological_Spaces.subseq everywhere? > > Thanks, > Andreas > > On 26/05/17 08:16, Tobias Nipkow wrote: >> Thank you for your research. I am perfectly happy with "sublist" (for >> the contiguous case) and "subseq" (for the general case) and think we >> should adopt it. >> >> [Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒ >> nat set ⇒ 'a list" (in List) to something else, eg sublist_index) >> >> Tobias >> >> On 25/05/2017 21:13, Jasmin Blanchette wrote: >>> >>>> On 25.05.2017, at 20:41, Tobias Nipkow <nip...@in.tum.de> wrote: >>>> >>>> I don't think that sublist, subsequence and substring really have >>>> much of a bias in either direction, except possibly substring, but >>>> the latter does indeed sound too specialized. >>> >>> Wikipedia has a clear bias (and I did not edit it, nor did I look it >>> up before writing my previous email): >>> >>> https://en.wikipedia.org/wiki/Subsequence >>> https://en.wikipedia.org/wiki/Substring >>> >>> Popular algorithm sbooks like Cormen et al. follow the same >>> definition of subsequence. Standard expressions like "longest >>> increasing subsequence" depend on this semantics. >>> >>> As for sublist, all the examples I see by Googling either "sublist", >>> "is_sublist", "isSublist", or "indexOfSubList" in Java, Python, >>> Scala, etc., have the contiguous semantics. Including this page: >>> >>> http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html >>> >>> I'm not saying we should rename the Isabelle concepts, just that >>> Isabelle is the odd (wo)man out. >>> >>> Jasmin >>> >> > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev