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