Re: [isabelle] New AFP theory: List Index



> 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.

Seconded!

I've been going on about this for years, but haven't been giving it high enough priority.

Gerwin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.