[isabelle-dev] [isabelle] Good name for "sublist" predicates
Lars Hupel
hupel at in.tum.de
Fri Jun 30 16:47:37 CEST 2017
> 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
More information about the isabelle-dev
mailing list