Re: [isabelle] New AFP theory: List Index
On Mon, 22 Feb 2010, Gerwin Klein wrote:
A feature that I often miss, especially considering namespace pollution
problems. One of the top-candidates on my wish list is something like
import-qualified, giving the user control over what symbols (and
syntax) will be loaded into the toplevel-namespace. Related to this
would be the possibility to specify the public interface of a theory.
Currently, the hide-command allows one to hide private symbols, but the
other way round would be more comfortable.
I've been going on about this for years, but haven't been giving it high
Well, I did give it a high priority, but it is technically very difficult.
In principle we already have sufficient infrastructure to control
visibility, or limit all kinds of "declarations" (syntax, hints to proof
tools) to a certain scope. It is all part of the "local theory"
Unfortunately, we are still stuck halfway in localizing everything -- this
refers to specification packages in the main library (datatype,
nominal_datatype etc.). Then the toplevel theory context can be treated
as just another local theory target, and benefit from additional control
over when and where declarations actually hit the user context.
I am in the middle of a major effort to work towards that again.
Nonetheless, it will take several more rounds to get there eventually.
Even worse, I recently see tendencies in user tools to forget about proper
locality and go back to global operations on the bare metal of the raw
This archive was generated by a fusion of
Pipermail (Mailman edition) and