[isabelle-dev] [isabelle] Good name for "sublist" predicates
andreas.lochbihler at inf.ethz.ch
Mon Jul 3 08:03:58 CEST 2017
Yes, it absolutely makes sense to change the situation with compact. It is a standard
notion in order theory, so my suggestion is to make it qualified with ccpo, just like
admissible and fixp are. I can take care of that.
On 30/06/17 21:31, Tobias Nipkow wrote:
> On 30/06/2017 20:41, Manuel Eberl wrote:
>>> By the way, I recently encountered a similar (and even more nasty)
>>> name clash, with compact. The following works perfectly
>> It's "Topological_Spaces.compact" and that should definitely work. We
>> should probably make the one from Complete_Partial_Order2 qualified. In
>> my opinion, there is no question that "compact" should be "compact" in
>> the topological sense.
> Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or renaming
> that "compact" in the most appropriate way.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev