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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev