> 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
bundle foo begin
notation Topological_Spaces.subseq ("subseq")
term "subseq f"
isabelle-dev mailing list