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.

This is a misunderstanding which exhibits the source of the problem:
syntax is not bound to namespaces but always global, which makes
pollution pervasive (c.f. the funny (no_)notation declarations for inf
and sup in the HOL theories -- an Isabelle joke...). We need finer
control over syntax here.

> Currently, the hide-command allows one to hide
> private symbols, but the other way round would be more comfortable.

I do not seed this demand as urgent: given that theory developers have
thought carefully which symbols ought to be hidden / qualified, the user
is always free to hide additional symbols when needed.

> If users want hierarchical module names, why don't we (the Isabelle
> developers) just implement that feature?

I agree that this is desirable.  But I suppose we first should find a
way to replace the rather archaic session concept by something which is
less driven by building descriptions in IsaMakefiles and ROOT.MLs, but
by the implicit structure of hierarchies.

A somehow related question is how to treat relative imports.  I recall
there has been (still is?) much debate on this in the Java and Python
community, and this has to be considered carefully (maybe inspired by

Tapping yet another barrel... ;-)



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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