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