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

[Makarius]

*** 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
specifications.


	Makarius