[isabelle-dev] NEWS: session-qualified theory names

Makarius makarius at sketis.net
Wed Apr 19 15:25:41 CEST 2017

*** General ***

* Theory names are qualified by the session name that they belong to.
This affects imports, but not the theory name space prefix: it remains
the theory base name as before. In order to import theories from other
sessions, the ROOT file format provides a new 'sessions' keyword. In
contrast, a theory that is imported in the old-fashioned manner via an
explicit file-system path belongs to the current session.

Theories that are imported from other sessions are excluded from the
current session document.

This refers to Isabelle/a72ab197e681.

After many small steps into that direction, it is a significant change
of user-relevant behavior. Next I will see how to move towards
standardized imports, without these slightly odd file-system path


More information about the isabelle-dev mailing list