> 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
