# HG changeset patch
# User wenzelm
# Date 1509713900 -3600
# Node ID 2c2a346cfe7038a623e98a0ba2e8fb2ec400a754
# Parent  69673025292efe932472a6f8d9f28f1f3d7d27cc
clarified situation of global theory names;

diff -r 69673025292e -r 2c2a346cfe70 NEWS
--- a/NEWS	Fri Nov 03 13:43:31 2017 +0100
+++ b/NEWS	Fri Nov 03 13:58:20 2017 +0100
@@ -14,6 +14,11 @@
 INCOMPATIBILITY for old developments that have not been updated to
 Isabelle2017 yet (using the "isabelle imports" tool).
 
+* Only the most fundamental theory names are global, usually the entry
+points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
+FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
+formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+
 * Command 'external_file' declares the formal dependency on the given
 file name, such that the Isabelle build process knows about it, but
 without specific Prover IDE management.
@@ -32,7 +37,8 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* Completion supports theory header imports.
+* Completion supports theory header imports, using theory base name.
+E.g. "Prob" is completed to "HOL-Probability.Probability".
 
 * The command-line tool "isabelle jedit" provides more flexible options
 for session selection:
diff -r 69673025292e -r 2c2a346cfe70 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Fri Nov 03 13:43:31 2017 +0100
+++ b/src/Doc/System/Sessions.thy	Fri Nov 03 13:58:20 2017 +0100
@@ -125,9 +125,12 @@
   \isakeyword{theories} block separately.
 
   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 graphs.
+  literally in other session specifications or theory imports --- the normal
+  situation is to qualify theory names by the session name; this ensures
+  globally unique names in big session graphs. Global theories are usually the
+  entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>,
+  \<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications
+  should not claim any global theory names.
 
   \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
   source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for