misc tuning and updates for release;
authorwenzelm
Wed Jun 06 14:14:37 2018 +0200 (11 months ago)
changeset 68393b9989df11c78
parent 68392 b2510432c94d
child 68394 bc2fd0e2047e
misc tuning and updates for release;
NEWS
     1.1 --- a/NEWS	Wed Jun 06 13:44:53 2018 +0200
     1.2 +++ b/NEWS	Wed Jun 06 14:14:37 2018 +0200
     1.3 @@ -9,6 +9,16 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Session-qualified theory names are mandatory: it is no longer possible
     1.8 +to refer to unqualified theories from the parent session.
     1.9 +INCOMPATIBILITY for old developments that have not been updated to
    1.10 +Isabelle2017 yet (using the "isabelle imports" tool).
    1.11 +
    1.12 +* Only the most fundamental theory names are global, usually the entry
    1.13 +points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
    1.14 +FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
    1.15 +formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
    1.16 +
    1.17  * Marginal comments need to be written exclusively in the new-style form
    1.18  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.19  supported. INCOMPATIBILITY, use the command-line tool "isabelle
    1.20 @@ -29,23 +39,9 @@
    1.21  In case you want to exclude conversion of ML files (because the tool
    1.22  frequently also converts ML's "op" syntax), use option "-m".
    1.23  
    1.24 -* The old 'def' command has been discontinued (legacy since
    1.25 -Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    1.26 -object-logic equality or equivalence.
    1.27 -
    1.28 -* Session-qualified theory names are mandatory: it is no longer possible
    1.29 -to refer to unqualified theories from the parent session.
    1.30 -INCOMPATIBILITY for old developments that have not been updated to
    1.31 -Isabelle2017 yet (using the "isabelle imports" tool).
    1.32 -
    1.33  * Theory header 'abbrevs' specifications need to be separated by 'and'.
    1.34  INCOMPATIBILITY.
    1.35  
    1.36 -* Only the most fundamental theory names are global, usually the entry
    1.37 -points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
    1.38 -FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
    1.39 -formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
    1.40 -
    1.41  * Command 'external_file' declares the formal dependency on the given
    1.42  file name, such that the Isabelle build process knows about it, but
    1.43  without specific Prover IDE management.
    1.44 @@ -64,13 +60,45 @@
    1.45  * The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
    1.46  use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
    1.47  
    1.48 -* Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to
    1.49 -avoid unclear meaning of the old "soft hyphen" U+00AD. Rare
    1.50 -INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.
    1.51 +* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
    1.52 +Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
    1.53 +U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
    1.54 +output.
    1.55  
    1.56  
    1.57  *** Isabelle/jEdit Prover IDE ***
    1.58  
    1.59 +* The command-line tool "isabelle jedit" provides more flexible options
    1.60 +for session management:
    1.61 +
    1.62 +  - option -R builds an auxiliary logic image with all required theories
    1.63 +    from other sessions, relative to an ancestor session given by option
    1.64 +    -A (default: parent)
    1.65 +
    1.66 +  - option -S is like -R, with a focus on the selected session and its
    1.67 +    descendants (this reduces startup time for big projects like AFP)
    1.68 +
    1.69 +  Examples:
    1.70 +    isabelle jedit -R HOL-Number_Theory
    1.71 +    isabelle jedit -R HOL-Number_Theory -A HOL
    1.72 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    1.73 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
    1.74 +
    1.75 +* PIDE markup for session ROOT files: allows to complete session names,
    1.76 +follow links to theories and document files etc.
    1.77 +
    1.78 +* Completion supports theory header imports, using theory base name.
    1.79 +E.g. "Prob" may be completed to "HOL-Probability.Probability".
    1.80 +
    1.81 +* Named control symbols (without special Unicode rendering) are shown as
    1.82 +bold-italic keyword. This is particularly useful for the short form of
    1.83 +antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
    1.84 +"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
    1.85 +arguments into this format.
    1.86 +
    1.87 +* Completion provides templates for named symbols with arguments,
    1.88 +e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
    1.89 +
    1.90  * Slightly more parallel checking, notably for high priority print
    1.91  functions (e.g. State output).
    1.92  
    1.93 @@ -82,37 +110,6 @@
    1.94  supersede former "spell_checker_elements" to determine regions of text
    1.95  that are subject to spell-checking. Minor INCOMPATIBILITY.
    1.96  
    1.97 -* PIDE markup for session ROOT files: allows to complete session names,
    1.98 -follow links to theories and document files etc.
    1.99 -
   1.100 -* Completion supports theory header imports, using theory base name.
   1.101 -E.g. "Prob" may be completed to "HOL-Probability.Probability".
   1.102 -
   1.103 -* The command-line tool "isabelle jedit" provides more flexible options
   1.104 -for session management:
   1.105 -  - option -R builds an auxiliary logic image with all required theories
   1.106 -    from other sessions, relative to an ancestor session given by option
   1.107 -    -A (default: parent)
   1.108 -  - option -S is like -R, with a focus on the selected session and its
   1.109 -    descendants (this reduces startup time for big projects like AFP)
   1.110 -
   1.111 -  Examples:
   1.112 -    isabelle jedit -R HOL-Number_Theory
   1.113 -    isabelle jedit -R HOL-Number_Theory -A HOL
   1.114 -    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
   1.115 -    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
   1.116 -
   1.117 -* Named control symbols (without special Unicode rendering) are shown as
   1.118 -bold-italic keyword. This is particularly useful for the short form of
   1.119 -antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
   1.120 -"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
   1.121 -arguments into this format.
   1.122 -
   1.123 -* Completion provides templates for named symbols with arguments,
   1.124 -e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
   1.125 -
   1.126 -* Bibtex database files (.bib) are semantically checked.
   1.127 -
   1.128  * Action "isabelle.preview" is able to present more file formats,
   1.129  notably bibtex database files and ML files.
   1.130  
   1.131 @@ -120,6 +117,8 @@
   1.132  plain-text document draft. Both are available via the menu "Plugins /
   1.133  Isabelle".
   1.134  
   1.135 +* Bibtex database files (.bib) are semantically checked.
   1.136 +
   1.137  * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
   1.138  is only used if there is no conflict with existing Unicode sequences in
   1.139  the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
   1.140 @@ -163,19 +162,23 @@
   1.141  antiquotations in control symbol notation, e.g. \<^const_name> becomes
   1.142  \isactrlconstUNDERSCOREname.
   1.143  
   1.144 -* Document antiquotation @{cite} now checks the given Bibtex entries
   1.145 -against the Bibtex database files -- only in batch-mode session builds.
   1.146 +* Document preparation with skip_proofs option now preserves the content
   1.147 +more accurately: only terminal proof steps ('by' etc.) are skipped.
   1.148  
   1.149  * Document antiquotation @{session name} checks and prints the given
   1.150  session name verbatim.
   1.151  
   1.152 -* Document preparation with skip_proofs option now preserves the content
   1.153 -more accurately: only terminal proof steps ('by' etc.) are skipped.
   1.154 +* Document antiquotation @{cite} now checks the given Bibtex entries
   1.155 +against the Bibtex database files -- only in batch-mode session builds.
   1.156  
   1.157  * Command-line tool "isabelle document" has been re-implemented in
   1.158  Isabelle/Scala, with simplified arguments and explicit errors from the
   1.159  latex and bibtex process. Minor INCOMPATIBILITY.
   1.160  
   1.161 +* Session ROOT entry: empty 'document_files' means there is no document
   1.162 +for this session. There is no need to specify options [document = false]
   1.163 +anymore.
   1.164 +
   1.165  
   1.166  *** Isar ***
   1.167  
   1.168 @@ -185,13 +188,17 @@
   1.169  Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
   1.170  (e.g. use 'find_theorems' or 'try' to figure this out).
   1.171  
   1.172 +* The old 'def' command has been discontinued (legacy since
   1.173 +Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
   1.174 +object-logic equality or equivalence.
   1.175 +
   1.176  * Rewrites clauses (keyword 'rewrites') were moved into the locale
   1.177 -expression syntax, where they are part of locale instances.  In
   1.178 -interpretation commands rewrites clauses now need to occur before
   1.179 -'for' and 'defines'.  Minor INCOMPATIBILITY.
   1.180 -
   1.181 -* For rewrites clauses, if activating a locale instance fails, fall
   1.182 -back to reading the clause first.  This helps avoid qualification of
   1.183 +expression syntax, where they are part of locale instances. In
   1.184 +interpretation commands rewrites clauses now need to occur before 'for'
   1.185 +and 'defines'. Minor INCOMPATIBILITY.
   1.186 +
   1.187 +* For 'rewrites' clauses, if activating a locale instance fails, fall
   1.188 +back to reading the clause first. This helps avoid qualification of
   1.189  locale instances where the qualifier's sole purpose is avoiding
   1.190  duplicate constant declarations.
   1.191  
   1.192 @@ -204,54 +211,55 @@
   1.193  
   1.194  *** HOL ***
   1.195  
   1.196 -* Landau_Symbols from the AFP was moved to HOL-Library
   1.197 -
   1.198  * Clarified relationship of characters, strings and code generation:
   1.199  
   1.200 -  * Type "char" is now a proper datatype of 8-bit values.
   1.201 -
   1.202 -  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
   1.203 -    general conversions "of_char" and "char_of" with suitable
   1.204 -    type constraints instead.
   1.205 -
   1.206 -  * The zero character is just written "CHR 0x00", not
   1.207 -    "0" any longer.
   1.208 -
   1.209 -  * Type "String.literal" (for code generation) is now isomorphic
   1.210 -    to lists of 7-bit (ASCII) values; concrete values can be written
   1.211 -    as "STR ''...''" for sequences of printable characters and
   1.212 -    "STR 0x..." for one single ASCII code point given
   1.213 -    as hexadecimal numeral.
   1.214 -
   1.215 -  * Type "String.literal" supports concatenation "... + ..."
   1.216 -    for all standard target languages.
   1.217 -
   1.218 -  * Theory Library/Code_Char is gone; study the explanations concerning
   1.219 -    "String.literal" in the tutorial on code generation to get an idea
   1.220 -    how target-language string literals can be converted to HOL string
   1.221 -    values and vice versa.
   1.222 -
   1.223 -  * Imperative-HOL: operation "raise" directly takes a value of type
   1.224 -    "String.literal" as argument, not type "string".
   1.225 -
   1.226 -INCOMPATIBILITY.
   1.227 -
   1.228 -* Abstract bit operations as part of Main: push_bit, take_bit,
   1.229 -drop_bit.
   1.230 -
   1.231 -* New, more general, axiomatization of complete_distrib_lattice.
   1.232 -The former axioms:
   1.233 -"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
   1.234 -are replaced by
   1.235 -"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
   1.236 -The instantiations of sets and functions as complete_distrib_lattice
   1.237 -are moved to Hilbert_Choice.thy because their proofs need the Hilbert
   1.238 -choice operator. The dual of this property is also proved in
   1.239 -Hilbert_Choice.thy.
   1.240 +  - Type "char" is now a proper datatype of 8-bit values.
   1.241 +
   1.242 +  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
   1.243 +    general conversions "of_char" and "char_of" with suitable type
   1.244 +    constraints instead.
   1.245 +
   1.246 +  - The zero character is just written "CHR 0x00", not "0" any longer.
   1.247 +
   1.248 +  - Type "String.literal" (for code generation) is now isomorphic to
   1.249 +    lists of 7-bit (ASCII) values; concrete values can be written as
   1.250 +    "STR ''...''" for sequences of printable characters and "STR 0x..."
   1.251 +    for one single ASCII code point given as hexadecimal numeral.
   1.252 +
   1.253 +  - Type "String.literal" supports concatenation "... + ..." for all
   1.254 +    standard target languages.
   1.255 +
   1.256 +  - Theory HOL-Library.Code_Char is gone; study the explanations
   1.257 +    concerning "String.literal" in the tutorial on code generation to
   1.258 +    get an idea how target-language string literals can be converted to
   1.259 +    HOL string values and vice versa.
   1.260 +
   1.261 +  - Session Imperative-HOL: operation "raise" directly takes a value of
   1.262 +    type "String.literal" as argument, not type "string".
   1.263 +
   1.264 +INCOMPATIBILITY.
   1.265 +
   1.266 +* Code generation: Code generation takes an explicit option
   1.267 +"case_insensitive" to accomodate case-insensitive file systems.
   1.268 +
   1.269 +* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
   1.270 +
   1.271 +* New, more general, axiomatization of complete_distrib_lattice. The
   1.272 +former axioms:
   1.273 +
   1.274 +  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
   1.275 +
   1.276 +are replaced by:
   1.277 +
   1.278 +  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
   1.279 +
   1.280 +The instantiations of sets and functions as complete_distrib_lattice are
   1.281 +moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
   1.282 +operator. The dual of this property is also proved in theory
   1.283 +HOL.Hilbert_Choice.
   1.284  
   1.285  * New syntax for the minimum/maximum of a function over a finite set:
   1.286 -MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
   1.287 -MAX.
   1.288 +MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
   1.289  
   1.290  * Clarifed theorem names:
   1.291  
   1.292 @@ -260,83 +268,59 @@
   1.293  
   1.294  Minor INCOMPATIBILITY.
   1.295  
   1.296 -* A new command parametric_constant for proving parametricity of
   1.297 -non-recursive definitions. For constants that are not fully parametric
   1.298 -the command will infer conditions on relations (e.g., bi_unique,
   1.299 -bi_total, or type class conditions such as "respects 0") sufficient for
   1.300 -parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
   1.301 -some examples.
   1.302 -
   1.303 -* A new preprocessor for the code generator to generate code for algebraic
   1.304 -  types with lazy evaluation semantics even in call-by-value target languages.
   1.305 -  See theory HOL-Library.Code_Lazy for the implementation and
   1.306 -  HOL-Codegenerator_Test.Code_Lazy_Test for examples.
   1.307 -
   1.308  * SMT module:
   1.309 +
   1.310    - The 'smt_oracle' option is now necessary when using the 'smt' method
   1.311      with a solver other than Z3. INCOMPATIBILITY.
   1.312 +
   1.313    - The encoding to first-order logic is now more complete in the
   1.314      presence of higher-order quantifiers. An 'smt_explicit_application'
   1.315      option has been added to control this. INCOMPATIBILITY.
   1.316  
   1.317 -* Datatypes:
   1.318 -  - The legacy command 'old_datatype', provided by
   1.319 -    '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
   1.320 -
   1.321 -* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
   1.322 -instances of rat, real, complex as factorial rings etc. Import
   1.323 -HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
   1.324 -INCOMPATIBILITY.
   1.325 -
   1.326  * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
   1.327  sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
   1.328  interpretation of abstract locales. INCOMPATIBILITY.
   1.329  
   1.330 +* Predicate coprime is now a real definition, not a mere abbreviation.
   1.331 +INCOMPATIBILITY.
   1.332 +
   1.333  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
   1.334  INCOMPATIBILITY.
   1.335  
   1.336  * The relator rel_filter on filters has been strengthened to its
   1.337 -canonical categorical definition with better properties. INCOMPATIBILITY.
   1.338 +canonical categorical definition with better properties.
   1.339 +INCOMPATIBILITY.
   1.340  
   1.341  * Generalized linear algebra involving linear, span, dependent, dim
   1.342  from type class real_vector to locales module and vector_space.
   1.343  Renamed:
   1.344 -  - span_inc ~> span_superset
   1.345 -  - span_superset ~> span_base
   1.346 -  - span_eq ~> span_eq_iff
   1.347 -INCOMPATIBILITY.
   1.348 -
   1.349 -* HOL-Algebra: renamed (^) to [^]
   1.350 -
   1.351 -* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
   1.352 -theorem, the Vitali covering theorem, change-of-variables results for
   1.353 -integration and measures.
   1.354 +
   1.355 +  span_inc ~> span_superset
   1.356 +  span_superset ~> span_base
   1.357 +  span_eq ~> span_eq_iff
   1.358 +
   1.359 +INCOMPATIBILITY.
   1.360  
   1.361  * Class linordered_semiring_1 covers zero_less_one also, ruling out
   1.362  pathologic instances. Minor INCOMPATIBILITY.
   1.363  
   1.364 -* Theory List: functions "sorted_wrt" and "sorted" now compare every
   1.365 -  element in a list to all following elements, not just the next one.
   1.366 -
   1.367 -* Theory List: Synatx:
   1.368 -  - filter-syntax "[x <- xs. P]" is no longer output syntax
   1.369 -    but only input syntax.
   1.370 -  - list comprehension syntax now supports tuple patterns in "pat <- xs".
   1.371 +* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
   1.372 +element in a list to all following elements, not just the next one.
   1.373 +
   1.374 +* Theory HOL.List syntax:
   1.375 +
   1.376 +  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
   1.377 +    input syntax
   1.378 +
   1.379 +  - list comprehension syntax now supports tuple patterns in "pat <- xs"
   1.380  
   1.381  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
   1.382  
   1.383 -* Predicate coprime is now a real definition, not a mere
   1.384 -abbreviation. INCOMPATIBILITY.
   1.385 -
   1.386 -* Code generation: Code generation takes an explicit option
   1.387 -"case_insensitive" to accomodate case-insensitive file systems.
   1.388 -
   1.389  * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
   1.390  clash with fact mod_mult_self4 (on more generic semirings).
   1.391  INCOMPATIBILITY.
   1.392  
   1.393  * Eliminated some theorem aliasses:
   1.394 -
   1.395    even_times_iff ~> even_mult_iff
   1.396    mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
   1.397    even_of_nat ~> even_int_iff
   1.398 @@ -344,18 +328,48 @@
   1.399  INCOMPATIBILITY.
   1.400  
   1.401  * Eliminated some theorem duplicate variations:
   1.402 -  * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
   1.403 -  * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
   1.404 -  * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
   1.405 -  * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
   1.406 -  * The witness of mod_eqD can be given directly as "_ div _".
   1.407 +
   1.408 +  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
   1.409 +  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
   1.410 +  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
   1.411 +  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
   1.412 +  - the witness of mod_eqD can be given directly as "_ div _"
   1.413  
   1.414  INCOMPATIBILITY.
   1.415  
   1.416  * Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
   1.417 -longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
   1.418 -adding "elim!: dvd" to classical proof methods in most situations
   1.419 -restores broken proofs.
   1.420 +longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
   1.421 +"elim!: dvd" to classical proof methods in most situations restores
   1.422 +broken proofs.
   1.423 +
   1.424 +* Theory HOL-Library.Conditional_Parametricity provides command
   1.425 +'parametric_constant' for proving parametricity of non-recursive
   1.426 +definitions. For constants that are not fully parametric the command
   1.427 +will infer conditions on relations (e.g., bi_unique, bi_total, or type
   1.428 +class conditions such as "respects 0") sufficient for parametricity. See
   1.429 +theory HOL-ex.Conditional_Parametricity_Examples for some examples.
   1.430 +
   1.431 +* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
   1.432 +generator to generate code for algebraic types with lazy evaluation
   1.433 +semantics even in call-by-value target languages. See theory
   1.434 +HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
   1.435 +
   1.436 +* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
   1.437 +
   1.438 +* Theory HOL-Library.Old_Datatype no longer provides the legacy command
   1.439 +'old_datatype'. INCOMPATIBILITY.
   1.440 +
   1.441 +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
   1.442 +instances of rat, real, complex as factorial rings etc. Import
   1.443 +HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
   1.444 +INCOMPATIBILITY.
   1.445 +
   1.446 +* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
   1.447 +infix/prefix notation.
   1.448 +
   1.449 +* Session HOL-Analysis: infinite products, Moebius functions, the
   1.450 +Riemann mapping theorem, the Vitali covering theorem,
   1.451 +change-of-variables results for integration and measures.
   1.452  
   1.453  
   1.454  *** ML ***
   1.455 @@ -371,47 +385,12 @@
   1.456  
   1.457  *** System ***
   1.458  
   1.459 -* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
   1.460 -heap images and session databases are always stored in
   1.461 -$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
   1.462 -$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
   1.463 -"isabelle jedit -s" or "isabelle build -s").
   1.464 -
   1.465 -* The command-line tool "export" and 'export_files' in session ROOT
   1.466 -entries retrieve theory exports from the session build database.
   1.467 -
   1.468 -* The command-line tools "isabelle server" and "isabelle client" provide
   1.469 -access to the Isabelle Server: it supports responsive session management
   1.470 -and concurrent use of theories, based on Isabelle/PIDE infrastructure.
   1.471 -See also the "system" manual.
   1.472 -
   1.473 -* The command-line tool "dump" dumps information from the cumulative
   1.474 -PIDE session database: many sessions may be loaded into a given logic
   1.475 -image, results from all loaded theories are written to the output
   1.476 -directory.
   1.477 -
   1.478 -* The command-line tool "isabelle update_comments" normalizes formal
   1.479 -comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
   1.480 -approximate the appearance in document output). This is more specific
   1.481 -than former "isabelle update_cartouches -c": the latter tool option has
   1.482 -been discontinued.
   1.483 -
   1.484 -* Session ROOT entry: empty 'document_files' means there is no document
   1.485 -for this session. There is no need to specify options [document = false]
   1.486 -anymore.
   1.487 -
   1.488 -* The command-line tool "isabelle mkroot" now always produces a document
   1.489 -outline: its options have been adapted accordingly. INCOMPATIBILITY.
   1.490 -
   1.491 -* The command-line tool "isabelle mkroot -I" initializes a Mercurial
   1.492 -repository for the generated session files.
   1.493 -
   1.494 -* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
   1.495 -support has been discontinued.
   1.496 -
   1.497  * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
   1.498  longer supported.
   1.499  
   1.500 +* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
   1.501 +support has been discontinued.
   1.502 +
   1.503  * Java runtime is for x86_64 only. Corresponding Isabelle settings have
   1.504  been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
   1.505  instead of former 32/64 variants. INCOMPATIBILITY.
   1.506 @@ -439,17 +418,46 @@
   1.507  corresponding environment values into account, when determining the
   1.508  up-to-date status of a session.
   1.509  
   1.510 +* The command-line tool "dump" dumps information from the cumulative
   1.511 +PIDE session database: many sessions may be loaded into a given logic
   1.512 +image, results from all loaded theories are written to the output
   1.513 +directory.
   1.514 +
   1.515  * Command-line tool "isabelle imports -I" also reports actual session
   1.516  imports. This helps to minimize the session dependency graph.
   1.517  
   1.518 -* Update to current Poly/ML 5.7.1 with slightly improved performance and
   1.519 -PIDE markup for identifier bindings.
   1.520 +* The command-line tool "export" and 'export_files' in session ROOT
   1.521 +entries retrieve theory exports from the session build database.
   1.522 +
   1.523 +* The command-line tools "isabelle server" and "isabelle client" provide
   1.524 +access to the Isabelle Server: it supports responsive session management
   1.525 +and concurrent use of theories, based on Isabelle/PIDE infrastructure.
   1.526 +See also the "system" manual.
   1.527 +
   1.528 +* The command-line tool "isabelle update_comments" normalizes formal
   1.529 +comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
   1.530 +approximate the appearance in document output). This is more specific
   1.531 +than former "isabelle update_cartouches -c": the latter tool option has
   1.532 +been discontinued.
   1.533 +
   1.534 +* The command-line tool "isabelle mkroot" now always produces a document
   1.535 +outline: its options have been adapted accordingly. INCOMPATIBILITY.
   1.536 +
   1.537 +* The command-line tool "isabelle mkroot -I" initializes a Mercurial
   1.538 +repository for the generated session files.
   1.539 +
   1.540 +* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
   1.541 +heap images and session databases are always stored in
   1.542 +$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
   1.543 +$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
   1.544 +"isabelle jedit -s" or "isabelle build -s").
   1.545  
   1.546  * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
   1.547  options for improved error reporting. Potential INCOMPATIBILITY with
   1.548  unusual LaTeX installations, may have to adapt these settings.
   1.549  
   1.550 -* The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision
   1.551 +* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
   1.552 +markup for identifier bindings. It now uses The GNU Multiple Precision
   1.553  Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
   1.554  32/64 bit.
   1.555