Re: [isabelle] New AFP theory: List Index
Tobias Nipkow wrote:
> My immediate plea is for modular library components. Having those as
> top-level entries dramatically increases the likelyhood that they are
> But you are quite right: Hackage offers some things worth emulating:
> - A listing of packages by category
> - cabal
> A complication is that Isabelle does not support hierarchical module
> names in the way Haskell (or Java or ...) does.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and