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