clarified situation of global theory names;
authorwenzelm
Fri Nov 03 13:58:20 2017 +0100 (18 months ago)
changeset 669932c2a346cfe70
parent 66992 69673025292e
child 66994 38fd865aae45
clarified situation of global theory names;
NEWS
src/Doc/System/Sessions.thy
     1.1 --- a/NEWS	Fri Nov 03 13:43:31 2017 +0100
     1.2 +++ b/NEWS	Fri Nov 03 13:58:20 2017 +0100
     1.3 @@ -14,6 +14,11 @@
     1.4  INCOMPATIBILITY for old developments that have not been updated to
     1.5  Isabelle2017 yet (using the "isabelle imports" tool).
     1.6  
     1.7 +* Only the most fundamental theory names are global, usually the entry
     1.8 +points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
     1.9 +FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
    1.10 +formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
    1.11 +
    1.12  * Command 'external_file' declares the formal dependency on the given
    1.13  file name, such that the Isabelle build process knows about it, but
    1.14  without specific Prover IDE management.
    1.15 @@ -32,7 +37,8 @@
    1.16  
    1.17  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.18  
    1.19 -* Completion supports theory header imports.
    1.20 +* Completion supports theory header imports, using theory base name.
    1.21 +E.g. "Prob" is completed to "HOL-Probability.Probability".
    1.22  
    1.23  * The command-line tool "isabelle jedit" provides more flexible options
    1.24  for session selection:
     2.1 --- a/src/Doc/System/Sessions.thy	Fri Nov 03 13:43:31 2017 +0100
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri Nov 03 13:58:20 2017 +0100
     2.3 @@ -125,9 +125,12 @@
     2.4    \isakeyword{theories} block separately.
     2.5  
     2.6    A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
     2.7 -  literally in other session specifications or theory imports. In contrast,
     2.8 -  the default is to qualify theory names by the session name, in order to
     2.9 -  ensure globally unique names in big session graphs.
    2.10 +  literally in other session specifications or theory imports --- the normal
    2.11 +  situation is to qualify theory names by the session name; this ensures
    2.12 +  globally unique names in big session graphs. Global theories are usually the
    2.13 +  entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>,
    2.14 +  \<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications
    2.15 +  should not claim any global theory names.
    2.16  
    2.17    \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
    2.18    source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for