However in packages often also bindings are created automatically.
Currently I am working on some fragements of a mechanism which analyzes
parts of a theory (most prominently constants and theorems) and
generated new constants and theorems from them. The result, in
particular the new
Florian Haftmann wrote:
What I have to address is that
you cannot be sure that a given name is already used, regardless how
many prefices you add.
There is a bit more to this story:
Ideally, the internals of a package should be completely invisible
unless a user explicitly chooses to look at
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
P foo
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a
