NEWS
changeset 66993 2c2a346cfe70
parent 66990 b23adab22e67
child 66994 38fd865aae45
     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: