# HG changeset patch
# User wenzelm
# Date 1492519906 -7200
# Node ID b80477da30ebb441014021bca9a91a5a0c10ecf5
# Parent  a3fffad8f21719899e1bf5234a10d8d8daad6aa5
some documentation;

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:
diff -r a3fffad8f217 -r b80477da30eb src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Apr 18 14:19:49 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Apr 18 14:51:46 2017 +0200
@@ -70,21 +70,24 @@
     ;
     value: @{syntax name} | @{syntax real}
     ;
-    theory_entry: @{syntax name} ('(' @'global' ')')?
+    sessions: @'sessions' (@{syntax name}+)
     ;
     theories: @'theories' opts? (theory_entry*)
     ;
+    theory_entry: @{syntax name} ('(' @'global' ')')?
+    ;
     files: @'files' (@{syntax name}+)
     ;
     document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
   \<close>}
 
   \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
-  parent session \<open>B\<close>, with its content given in \<open>body\<close> (theories and auxiliary
-  source files). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
-  applications: only Isabelle/Pure can bootstrap itself from nothing.
+  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
+  theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
+  mandatory in practical applications: only Isabelle/Pure can bootstrap itself
+  from nothing.
 
-  All such session specifications together describe a hierarchy (tree) of
+  All such session specifications together describe a hierarchy (graph) of
   sessions, with globally unique names. The new session name \<open>A\<close> should be
   sufficiently long and descriptive to stand on its own in a potentially large
   library.
@@ -112,6 +115,12 @@
   but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
   true\<close> for Boolean options.
 
+  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
+  the current name space of theories. This allows to refer to a theory \<open>A\<close>
+  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
+  into the current ML process, which is in contrast to a theory that is
+  already present in the \<^emph>\<open>parent\<close> session.
+
   \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
   are processed within an environment that is augmented by the given options,
   in addition to the global session options given before. Any number of blocks
@@ -121,7 +130,7 @@
   A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
   literally in other session specifications or theory imports. In contrast,
   the default is to qualify theory names by the session name, in order to
-  ensure globally unique names in big session trees.
+  ensure globally unique names in big session graphs.
 
   \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
   in the processing of this session. This should cover anything outside the