diff -r a3fffad8f217 -r b80477da30eb NEWS
--- a/NEWS	Tue Apr 18 14:19:49 2017 +0200
+++ b/NEWS	Tue Apr 18 14:51:46 2017 +0200
@@ -9,6 +9,13 @@
 
 *** 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.
+
 * The main theory entry points for some non-HOL sessions have changed,
 to avoid confusion with the global name "Main" of the session HOL. This
 leads to the follow renamings: