[isabelle-dev] HOL-Algebra

[Makarius]

On 12/05/18 11:40, Lawrence Paulson wrote:
> I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are
> ancient. They desperately need updating and streamlining.
> 
> We’ve decided that Group-Ring-Module is irremediable, and are using it
> only as a list of useful results that need to be done again.

Just one oddity in HOL-Algebra: It claims canonical theory names like
"Group", "Ring", "Module". Thus the main HOL session needs to evade via
non-standard names "Groups", "Rings", "Modules" (the latter is new in
2af1f142f855).


Just for theory names, we now have session-qualifiers, i.e. HOL.Group
vs. HOL-Algebra.Group would work, but the internal name spaces are not
qualified separately, and a merge does not work.

At some point, I would like to see the long theory name also as internal
name space qualifier, e.g. "HOL-Algebra.Group", but there are some
remaining problems:

  * It needs to be implemented properly, in particular for tools that
pretend to know Isabelle name space policies (by analyzing the structure
of full names).

  * Non-identifiers as session names are bad, e.g. a constant name
HOL-Algebra.Group.group cannot be used within a term. We would have to
rename many sessions. This is particularly difficult in AFP, where
session names and entry names (with resulting URLs) should usually coincide.


	Makarius