NEWS
changeset 66789 feb36b73a7f0
parent 66786 61617dafcd60
parent 66768 f27488f47a47
child 66801 f3fda9777f9a
     1.1 --- a/NEWS	Sun Oct 08 11:58:01 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 14:48:47 2017 +0200
     1.3 @@ -4,6 +4,57 @@
     1.4  (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     1.5  
     1.6  
     1.7 +New in this Isabelle version
     1.8 +----------------------------
     1.9 +
    1.10 +*** General ***
    1.11 +
    1.12 +* Session-qualified theory names are mandatory: it is no longer possible
    1.13 +to refer to unqualified theories from the parent session.
    1.14 +INCOMPATIBILITY for old developments that have not been updated to
    1.15 +Isabelle2017 yet (using the "isabelle imports" tool).
    1.16 +
    1.17 +* Command 'external_file' declares the formal dependency on the given
    1.18 +file name, such that the Isabelle build process knows about it, but
    1.19 +without specific Prover IDE management.
    1.20 +
    1.21 +* Session ROOT entries no longer allow specification of 'files'. Rare
    1.22 +INCOMPATIBILITY, use command 'external_file' within a proper theory
    1.23 +context.
    1.24 +
    1.25 +* Session root directories may be specified multiple times: each
    1.26 +accessible ROOT file is processed only once. This facilitates
    1.27 +specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
    1.28 +-d or -D for "isabelle build" and "isabelle jedit". Example:
    1.29 +
    1.30 +  isabelle build -D '~~/src/ZF'
    1.31 +
    1.32 +
    1.33 +*** Prover IDE -- Isabelle/Scala/jEdit ***
    1.34 +
    1.35 +* Completion supports theory header imports.
    1.36 +
    1.37 +
    1.38 +*** HOL ***
    1.39 +
    1.40 +* SMT module:
    1.41 +  - The 'smt_oracle' option is now necessary when using the 'smt' method
    1.42 +    with a solver other than Z3. INCOMPATIBILITY.
    1.43 +  - The encoding to first-order logic is now more complete in the presence of
    1.44 +    higher-order quantifiers. An 'smt_explicit_application' option has been
    1.45 +    added to control this. INCOMPATIBILITY.
    1.46 +
    1.47 +
    1.48 +*** System ***
    1.49 +
    1.50 +* Windows and Cygwin is for x86_64 only. Old 32bit platform support has
    1.51 +been discontinued.
    1.52 +
    1.53 +* Command-line tool "isabelle build" supports new options:
    1.54 +  - option -B NAME: include session NAME and all descendants
    1.55 +  - option -S: only observe changes of sources, not heap images
    1.56 +
    1.57 +
    1.58  New in Isabelle2017 (October 2017)
    1.59  ----------------------------------
    1.60