[isabelle-dev] [isabelle] Good name for "sublist" predicates

[Lars Hupel]

> Incidentally, I wonder if it is possible to locally prefer one of the
> two constants, i.e. say that, in the following block, I want "subseq" to
> mean "Topological_Spaces.subseq". That might also mitigate the problem
> of long qualified names.

Here's my unqualified opinion: Makarius already introduced the "bundle"
target that allows us to specify syntax and declarations. Maybe this
could be extended to somehow influence naming policy?

The following is possible today, but I doubt that this is a desired
solution:

bundle foo begin
  notation Topological_Spaces.subseq ("subseq")
end

context
  includes foo
begin

term "subseq f"

end

Cheers
Lars