Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle] Isabelle theory name clash

Email Gateway (Jul 14 2026 at 10:00):

From: Makarius <makarius@sketis.net>

On 13/07/2026 12:46, Lawrence Paulson wrote:

This is a tough ons, but we need a migration plan to make theory names local
to sessions somehow.

We have that already. See this NEWS entry from Isabelle2017 (October 2017):

"""

• Theory names are qualified by the session name that they belong to.
  This affects imports, but not the theory name space prefix (which is
  just the theory base name as before).
  """

The remaining problem are the internal name spaces of theories. It will work
properly "one happy day in the near future". One problem here is that we have
more and more funny Isabelle/ML tools doing odd things with internal names.
Thus it becomes increasingly difficult to cleanup things. It will happen
nonetheless, eventually.

Makarius

Last updated: Aug 05 2026 at 21:11 UTC