merged
authorwenzelm
Wed Jun 06 14:23:13 2018 +0200 (12 months ago)
changeset 68398194fa3d2d6a4
parent 68387 691c02d1699b
parent 68397 cace81744c61
child 68400 cada19e0c6c7
child 68401 cd53ad6e7d96
merged
     1.1 --- a/ANNOUNCE	Wed Jun 06 13:04:52 2018 +0200
     1.2 +++ b/ANNOUNCE	Wed Jun 06 14:23:13 2018 +0200
     1.3 @@ -1,32 +1,15 @@
     1.4 -Subject: Announcing Isabelle2017
     1.5 +Subject: Announcing Isabelle2018
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2017 is now available.
     1.9 +Isabelle2018 is now available.
    1.10  
    1.11 -This version introduces many changes over Isabelle2016-1: see the NEWS
    1.12 +This version introduces many changes over Isabelle2017: see the NEWS
    1.13  file for further details. Some notable points:
    1.14  
    1.15 -* Experimental support for Visual Studio Code as alternative PIDE front-end.
    1.16 -
    1.17 -* Improved Isabelle/jEdit Prover IDE: management of session sources
    1.18 -independently of editor buffers, removal of unused theories, explicit
    1.19 -indication of theory status, more careful auto-indentation.
    1.20 -
    1.21 -* Session-qualified theory imports.
    1.22 -
    1.23 -* Code generator improvements: support for statically embedded computations.
    1.24 -
    1.25 -* Numerous HOL library improvements.
    1.26 -
    1.27 -* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
    1.28 -(ported from HOL-Light).
    1.29 -
    1.30 -* Improved Nunchaku model finder, now in main HOL.
    1.31 -
    1.32 -* SQL database support in Isabelle/Scala.
    1.33 +* FIXME.
    1.34  
    1.35  
    1.36 -You may get Isabelle2017 from the following mirror sites:
    1.37 +You may get Isabelle2018 from the following mirror sites:
    1.38  
    1.39    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle
    1.40    Munich (Germany)     http://isabelle.in.tum.de
     2.1 --- a/Admin/components/components.sha1	Wed Jun 06 13:04:52 2018 +0200
     2.2 +++ b/Admin/components/components.sha1	Wed Jun 06 14:23:13 2018 +0200
     2.3 @@ -215,6 +215,7 @@
     2.4  b016a785f1f78855c00d351ff598355c3b87450f  sqlite-jdbc-3.18.0-1.tar.gz
     2.5  b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf  sqlite-jdbc-3.18.0.tar.gz
     2.6  e56117a67ab01fb24c7fc054ede3160cefdac5f8  sqlite-jdbc-3.20.0.tar.gz
     2.7 +27aeac6a91353d69f0438837798ac4ae6f9ff8c5  sqlite-jdbc-3.23.1.tar.gz
     2.8  8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
     2.9  2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
    2.10  1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
     3.1 --- a/Admin/components/main	Wed Jun 06 13:04:52 2018 +0200
     3.2 +++ b/Admin/components/main	Wed Jun 06 14:23:13 2018 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4  smbc-0.4.1
     3.5  ssh-java-20161009
     3.6  spass-3.8ds-1
     3.7 -sqlite-jdbc-3.20.0
     3.8 +sqlite-jdbc-3.23.1
     3.9  verit-2016post
    3.10  xz-java-1.8
    3.11  z3-4.4.0pre-2
     4.1 --- a/CONTRIBUTORS	Wed Jun 06 13:04:52 2018 +0200
     4.2 +++ b/CONTRIBUTORS	Wed Jun 06 14:23:13 2018 +0200
     4.3 @@ -3,11 +3,11 @@
     4.4  listed as an author in one of the source files of this Isabelle distribution.
     4.5  
     4.6  
     4.7 -Contributions to this Isabelle version
     4.8 ---------------------------------------
     4.9 +Contributions to Isabelle2018
    4.10 +-----------------------------
    4.11  
    4.12  * May 2018: Manuel Eberl
    4.13 -  Landau symbols and asymptotic equivalence (moved from the AFP)
    4.14 +  Landau symbols and asymptotic equivalence (moved from the AFP).
    4.15  
    4.16  * May 2018: Jose Divasón (Universidad de la Rioja),
    4.17    Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
    4.18 @@ -22,9 +22,8 @@
    4.19    Code generation with lazy evaluation semantics.
    4.20  
    4.21  * March 2018: Florian Haftmann
    4.22 -  Abstract bit operations push_bit, take_bit, drop_bit, alongside
    4.23 -  with an algebraic foundation for bit strings and word types in
    4.24 -  HOL-ex.
    4.25 +  Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
    4.26 +  algebraic foundation for bit strings and word types in HOL-ex.
    4.27  
    4.28  * March 2018: Viorel Preoteasa
    4.29    Generalisation of complete_distrib_lattice
    4.30 @@ -36,7 +35,8 @@
    4.31    A new conditional parametricity prover.
    4.32  
    4.33  * October 2017: Alexander Maletzky
    4.34 -  Derivation of axiom "iff" in HOL.thy from the other axioms.
    4.35 +  Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
    4.36 +
    4.37  
    4.38  Contributions to Isabelle2017
    4.39  -----------------------------
     5.1 --- a/COPYRIGHT	Wed Jun 06 13:04:52 2018 +0200
     5.2 +++ b/COPYRIGHT	Wed Jun 06 14:23:13 2018 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
     5.5  
     5.6 -Copyright (c) 1986-2017,
     5.7 +Copyright (c) 1986-2018,
     5.8    University of Cambridge,
     5.9    Technische Universitaet Muenchen,
    5.10    and contributors.
     6.1 --- a/NEWS	Wed Jun 06 13:04:52 2018 +0200
     6.2 +++ b/NEWS	Wed Jun 06 14:23:13 2018 +0200
     6.3 @@ -4,11 +4,21 @@
     6.4  (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     6.5  
     6.6  
     6.7 -New in this Isabelle version
     6.8 -----------------------------
     6.9 +New in Isabelle2018 (August 2018)
    6.10 +---------------------------------
    6.11  
    6.12  *** General ***
    6.13  
    6.14 +* Session-qualified theory names are mandatory: it is no longer possible
    6.15 +to refer to unqualified theories from the parent session.
    6.16 +INCOMPATIBILITY for old developments that have not been updated to
    6.17 +Isabelle2017 yet (using the "isabelle imports" tool).
    6.18 +
    6.19 +* Only the most fundamental theory names are global, usually the entry
    6.20 +points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
    6.21 +FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
    6.22 +formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
    6.23 +
    6.24  * Marginal comments need to be written exclusively in the new-style form
    6.25  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    6.26  supported. INCOMPATIBILITY, use the command-line tool "isabelle
    6.27 @@ -29,23 +39,9 @@
    6.28  In case you want to exclude conversion of ML files (because the tool
    6.29  frequently also converts ML's "op" syntax), use option "-m".
    6.30  
    6.31 -* The old 'def' command has been discontinued (legacy since
    6.32 -Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    6.33 -object-logic equality or equivalence.
    6.34 -
    6.35 -* Session-qualified theory names are mandatory: it is no longer possible
    6.36 -to refer to unqualified theories from the parent session.
    6.37 -INCOMPATIBILITY for old developments that have not been updated to
    6.38 -Isabelle2017 yet (using the "isabelle imports" tool).
    6.39 -
    6.40  * Theory header 'abbrevs' specifications need to be separated by 'and'.
    6.41  INCOMPATIBILITY.
    6.42  
    6.43 -* Only the most fundamental theory names are global, usually the entry
    6.44 -points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
    6.45 -FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
    6.46 -formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
    6.47 -
    6.48  * Command 'external_file' declares the formal dependency on the given
    6.49  file name, such that the Isabelle build process knows about it, but
    6.50  without specific Prover IDE management.
    6.51 @@ -64,13 +60,45 @@
    6.52  * The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
    6.53  use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
    6.54  
    6.55 -* Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to
    6.56 -avoid unclear meaning of the old "soft hyphen" U+00AD. Rare
    6.57 -INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.
    6.58 +* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
    6.59 +Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
    6.60 +U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
    6.61 +output.
    6.62  
    6.63  
    6.64  *** Isabelle/jEdit Prover IDE ***
    6.65  
    6.66 +* The command-line tool "isabelle jedit" provides more flexible options
    6.67 +for session management:
    6.68 +
    6.69 +  - option -R builds an auxiliary logic image with all required theories
    6.70 +    from other sessions, relative to an ancestor session given by option
    6.71 +    -A (default: parent)
    6.72 +
    6.73 +  - option -S is like -R, with a focus on the selected session and its
    6.74 +    descendants (this reduces startup time for big projects like AFP)
    6.75 +
    6.76 +  Examples:
    6.77 +    isabelle jedit -R HOL-Number_Theory
    6.78 +    isabelle jedit -R HOL-Number_Theory -A HOL
    6.79 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    6.80 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
    6.81 +
    6.82 +* PIDE markup for session ROOT files: allows to complete session names,
    6.83 +follow links to theories and document files etc.
    6.84 +
    6.85 +* Completion supports theory header imports, using theory base name.
    6.86 +E.g. "Prob" may be completed to "HOL-Probability.Probability".
    6.87 +
    6.88 +* Named control symbols (without special Unicode rendering) are shown as
    6.89 +bold-italic keyword. This is particularly useful for the short form of
    6.90 +antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
    6.91 +"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
    6.92 +arguments into this format.
    6.93 +
    6.94 +* Completion provides templates for named symbols with arguments,
    6.95 +e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
    6.96 +
    6.97  * Slightly more parallel checking, notably for high priority print
    6.98  functions (e.g. State output).
    6.99  
   6.100 @@ -82,37 +110,6 @@
   6.101  supersede former "spell_checker_elements" to determine regions of text
   6.102  that are subject to spell-checking. Minor INCOMPATIBILITY.
   6.103  
   6.104 -* PIDE markup for session ROOT files: allows to complete session names,
   6.105 -follow links to theories and document files etc.
   6.106 -
   6.107 -* Completion supports theory header imports, using theory base name.
   6.108 -E.g. "Prob" may be completed to "HOL-Probability.Probability".
   6.109 -
   6.110 -* The command-line tool "isabelle jedit" provides more flexible options
   6.111 -for session management:
   6.112 -  - option -R builds an auxiliary logic image with all required theories
   6.113 -    from other sessions, relative to an ancestor session given by option
   6.114 -    -A (default: parent)
   6.115 -  - option -S is like -R, with a focus on the selected session and its
   6.116 -    descendants (this reduces startup time for big projects like AFP)
   6.117 -
   6.118 -  Examples:
   6.119 -    isabelle jedit -R HOL-Number_Theory
   6.120 -    isabelle jedit -R HOL-Number_Theory -A HOL
   6.121 -    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
   6.122 -    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
   6.123 -
   6.124 -* Named control symbols (without special Unicode rendering) are shown as
   6.125 -bold-italic keyword. This is particularly useful for the short form of
   6.126 -antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
   6.127 -"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
   6.128 -arguments into this format.
   6.129 -
   6.130 -* Completion provides templates for named symbols with arguments,
   6.131 -e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
   6.132 -
   6.133 -* Bibtex database files (.bib) are semantically checked.
   6.134 -
   6.135  * Action "isabelle.preview" is able to present more file formats,
   6.136  notably bibtex database files and ML files.
   6.137  
   6.138 @@ -120,6 +117,8 @@
   6.139  plain-text document draft. Both are available via the menu "Plugins /
   6.140  Isabelle".
   6.141  
   6.142 +* Bibtex database files (.bib) are semantically checked.
   6.143 +
   6.144  * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
   6.145  is only used if there is no conflict with existing Unicode sequences in
   6.146  the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
   6.147 @@ -163,19 +162,23 @@
   6.148  antiquotations in control symbol notation, e.g. \<^const_name> becomes
   6.149  \isactrlconstUNDERSCOREname.
   6.150  
   6.151 -* Document antiquotation @{cite} now checks the given Bibtex entries
   6.152 -against the Bibtex database files -- only in batch-mode session builds.
   6.153 +* Document preparation with skip_proofs option now preserves the content
   6.154 +more accurately: only terminal proof steps ('by' etc.) are skipped.
   6.155  
   6.156  * Document antiquotation @{session name} checks and prints the given
   6.157  session name verbatim.
   6.158  
   6.159 -* Document preparation with skip_proofs option now preserves the content
   6.160 -more accurately: only terminal proof steps ('by' etc.) are skipped.
   6.161 +* Document antiquotation @{cite} now checks the given Bibtex entries
   6.162 +against the Bibtex database files -- only in batch-mode session builds.
   6.163  
   6.164  * Command-line tool "isabelle document" has been re-implemented in
   6.165  Isabelle/Scala, with simplified arguments and explicit errors from the
   6.166  latex and bibtex process. Minor INCOMPATIBILITY.
   6.167  
   6.168 +* Session ROOT entry: empty 'document_files' means there is no document
   6.169 +for this session. There is no need to specify options [document = false]
   6.170 +anymore.
   6.171 +
   6.172  
   6.173  *** Isar ***
   6.174  
   6.175 @@ -185,13 +188,17 @@
   6.176  Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
   6.177  (e.g. use 'find_theorems' or 'try' to figure this out).
   6.178  
   6.179 +* The old 'def' command has been discontinued (legacy since
   6.180 +Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
   6.181 +object-logic equality or equivalence.
   6.182 +
   6.183  * Rewrites clauses (keyword 'rewrites') were moved into the locale
   6.184 -expression syntax, where they are part of locale instances.  In
   6.185 -interpretation commands rewrites clauses now need to occur before
   6.186 -'for' and 'defines'.  Minor INCOMPATIBILITY.
   6.187 -
   6.188 -* For rewrites clauses, if activating a locale instance fails, fall
   6.189 -back to reading the clause first.  This helps avoid qualification of
   6.190 +expression syntax, where they are part of locale instances. In
   6.191 +interpretation commands rewrites clauses now need to occur before 'for'
   6.192 +and 'defines'. Minor INCOMPATIBILITY.
   6.193 +
   6.194 +* For 'rewrites' clauses, if activating a locale instance fails, fall
   6.195 +back to reading the clause first. This helps avoid qualification of
   6.196  locale instances where the qualifier's sole purpose is avoiding
   6.197  duplicate constant declarations.
   6.198  
   6.199 @@ -204,54 +211,55 @@
   6.200  
   6.201  *** HOL ***
   6.202  
   6.203 -* Landau_Symbols from the AFP was moved to HOL-Library
   6.204 -
   6.205  * Clarified relationship of characters, strings and code generation:
   6.206  
   6.207 -  * Type "char" is now a proper datatype of 8-bit values.
   6.208 -
   6.209 -  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
   6.210 -    general conversions "of_char" and "char_of" with suitable
   6.211 -    type constraints instead.
   6.212 -
   6.213 -  * The zero character is just written "CHR 0x00", not
   6.214 -    "0" any longer.
   6.215 -
   6.216 -  * Type "String.literal" (for code generation) is now isomorphic
   6.217 -    to lists of 7-bit (ASCII) values; concrete values can be written
   6.218 -    as "STR ''...''" for sequences of printable characters and
   6.219 -    "STR 0x..." for one single ASCII code point given
   6.220 -    as hexadecimal numeral.
   6.221 -
   6.222 -  * Type "String.literal" supports concatenation "... + ..."
   6.223 -    for all standard target languages.
   6.224 -
   6.225 -  * Theory Library/Code_Char is gone; study the explanations concerning
   6.226 -    "String.literal" in the tutorial on code generation to get an idea
   6.227 -    how target-language string literals can be converted to HOL string
   6.228 -    values and vice versa.
   6.229 -
   6.230 -  * Imperative-HOL: operation "raise" directly takes a value of type
   6.231 -    "String.literal" as argument, not type "string".
   6.232 -
   6.233 -INCOMPATIBILITY.
   6.234 -
   6.235 -* Abstract bit operations as part of Main: push_bit, take_bit,
   6.236 -drop_bit.
   6.237 -
   6.238 -* New, more general, axiomatization of complete_distrib_lattice.
   6.239 -The former axioms:
   6.240 -"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
   6.241 -are replaced by
   6.242 -"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
   6.243 -The instantiations of sets and functions as complete_distrib_lattice
   6.244 -are moved to Hilbert_Choice.thy because their proofs need the Hilbert
   6.245 -choice operator. The dual of this property is also proved in
   6.246 -Hilbert_Choice.thy.
   6.247 +  - Type "char" is now a proper datatype of 8-bit values.
   6.248 +
   6.249 +  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
   6.250 +    general conversions "of_char" and "char_of" with suitable type
   6.251 +    constraints instead.
   6.252 +
   6.253 +  - The zero character is just written "CHR 0x00", not "0" any longer.
   6.254 +
   6.255 +  - Type "String.literal" (for code generation) is now isomorphic to
   6.256 +    lists of 7-bit (ASCII) values; concrete values can be written as
   6.257 +    "STR ''...''" for sequences of printable characters and "STR 0x..."
   6.258 +    for one single ASCII code point given as hexadecimal numeral.
   6.259 +
   6.260 +  - Type "String.literal" supports concatenation "... + ..." for all
   6.261 +    standard target languages.
   6.262 +
   6.263 +  - Theory HOL-Library.Code_Char is gone; study the explanations
   6.264 +    concerning "String.literal" in the tutorial on code generation to
   6.265 +    get an idea how target-language string literals can be converted to
   6.266 +    HOL string values and vice versa.
   6.267 +
   6.268 +  - Session Imperative-HOL: operation "raise" directly takes a value of
   6.269 +    type "String.literal" as argument, not type "string".
   6.270 +
   6.271 +INCOMPATIBILITY.
   6.272 +
   6.273 +* Code generation: Code generation takes an explicit option
   6.274 +"case_insensitive" to accomodate case-insensitive file systems.
   6.275 +
   6.276 +* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
   6.277 +
   6.278 +* New, more general, axiomatization of complete_distrib_lattice. The
   6.279 +former axioms:
   6.280 +
   6.281 +  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
   6.282 +
   6.283 +are replaced by:
   6.284 +
   6.285 +  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
   6.286 +
   6.287 +The instantiations of sets and functions as complete_distrib_lattice are
   6.288 +moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
   6.289 +operator. The dual of this property is also proved in theory
   6.290 +HOL.Hilbert_Choice.
   6.291  
   6.292  * New syntax for the minimum/maximum of a function over a finite set:
   6.293 -MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
   6.294 -MAX.
   6.295 +MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
   6.296  
   6.297  * Clarifed theorem names:
   6.298  
   6.299 @@ -260,83 +268,59 @@
   6.300  
   6.301  Minor INCOMPATIBILITY.
   6.302  
   6.303 -* A new command parametric_constant for proving parametricity of
   6.304 -non-recursive definitions. For constants that are not fully parametric
   6.305 -the command will infer conditions on relations (e.g., bi_unique,
   6.306 -bi_total, or type class conditions such as "respects 0") sufficient for
   6.307 -parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
   6.308 -some examples.
   6.309 -
   6.310 -* A new preprocessor for the code generator to generate code for algebraic
   6.311 -  types with lazy evaluation semantics even in call-by-value target languages.
   6.312 -  See theory HOL-Library.Code_Lazy for the implementation and
   6.313 -  HOL-Codegenerator_Test.Code_Lazy_Test for examples.
   6.314 -
   6.315  * SMT module:
   6.316 +
   6.317    - The 'smt_oracle' option is now necessary when using the 'smt' method
   6.318      with a solver other than Z3. INCOMPATIBILITY.
   6.319 +
   6.320    - The encoding to first-order logic is now more complete in the
   6.321      presence of higher-order quantifiers. An 'smt_explicit_application'
   6.322      option has been added to control this. INCOMPATIBILITY.
   6.323  
   6.324 -* Datatypes:
   6.325 -  - The legacy command 'old_datatype', provided by
   6.326 -    '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
   6.327 -
   6.328 -* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
   6.329 -instances of rat, real, complex as factorial rings etc. Import
   6.330 -HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
   6.331 -INCOMPATIBILITY.
   6.332 -
   6.333  * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
   6.334  sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
   6.335  interpretation of abstract locales. INCOMPATIBILITY.
   6.336  
   6.337 +* Predicate coprime is now a real definition, not a mere abbreviation.
   6.338 +INCOMPATIBILITY.
   6.339 +
   6.340  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
   6.341  INCOMPATIBILITY.
   6.342  
   6.343  * The relator rel_filter on filters has been strengthened to its
   6.344 -canonical categorical definition with better properties. INCOMPATIBILITY.
   6.345 +canonical categorical definition with better properties.
   6.346 +INCOMPATIBILITY.
   6.347  
   6.348  * Generalized linear algebra involving linear, span, dependent, dim
   6.349  from type class real_vector to locales module and vector_space.
   6.350  Renamed:
   6.351 -  - span_inc ~> span_superset
   6.352 -  - span_superset ~> span_base
   6.353 -  - span_eq ~> span_eq_iff
   6.354 -INCOMPATIBILITY.
   6.355 -
   6.356 -* HOL-Algebra: renamed (^) to [^]
   6.357 -
   6.358 -* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
   6.359 -theorem, the Vitali covering theorem, change-of-variables results for
   6.360 -integration and measures.
   6.361 +
   6.362 +  span_inc ~> span_superset
   6.363 +  span_superset ~> span_base
   6.364 +  span_eq ~> span_eq_iff
   6.365 +
   6.366 +INCOMPATIBILITY.
   6.367  
   6.368  * Class linordered_semiring_1 covers zero_less_one also, ruling out
   6.369  pathologic instances. Minor INCOMPATIBILITY.
   6.370  
   6.371 -* Theory List: functions "sorted_wrt" and "sorted" now compare every
   6.372 -  element in a list to all following elements, not just the next one.
   6.373 -
   6.374 -* Theory List: Synatx:
   6.375 -  - filter-syntax "[x <- xs. P]" is no longer output syntax
   6.376 -    but only input syntax.
   6.377 -  - list comprehension syntax now supports tuple patterns in "pat <- xs".
   6.378 +* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
   6.379 +element in a list to all following elements, not just the next one.
   6.380 +
   6.381 +* Theory HOL.List syntax:
   6.382 +
   6.383 +  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
   6.384 +    input syntax
   6.385 +
   6.386 +  - list comprehension syntax now supports tuple patterns in "pat <- xs"
   6.387  
   6.388  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
   6.389  
   6.390 -* Predicate coprime is now a real definition, not a mere
   6.391 -abbreviation. INCOMPATIBILITY.
   6.392 -
   6.393 -* Code generation: Code generation takes an explicit option
   6.394 -"case_insensitive" to accomodate case-insensitive file systems.
   6.395 -
   6.396  * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
   6.397  clash with fact mod_mult_self4 (on more generic semirings).
   6.398  INCOMPATIBILITY.
   6.399  
   6.400  * Eliminated some theorem aliasses:
   6.401 -
   6.402    even_times_iff ~> even_mult_iff
   6.403    mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
   6.404    even_of_nat ~> even_int_iff
   6.405 @@ -344,18 +328,48 @@
   6.406  INCOMPATIBILITY.
   6.407  
   6.408  * Eliminated some theorem duplicate variations:
   6.409 -  * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
   6.410 -  * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
   6.411 -  * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
   6.412 -  * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
   6.413 -  * The witness of mod_eqD can be given directly as "_ div _".
   6.414 +
   6.415 +  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
   6.416 +  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
   6.417 +  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
   6.418 +  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
   6.419 +  - the witness of mod_eqD can be given directly as "_ div _"
   6.420  
   6.421  INCOMPATIBILITY.
   6.422  
   6.423  * Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
   6.424 -longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
   6.425 -adding "elim!: dvd" to classical proof methods in most situations
   6.426 -restores broken proofs.
   6.427 +longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
   6.428 +"elim!: dvd" to classical proof methods in most situations restores
   6.429 +broken proofs.
   6.430 +
   6.431 +* Theory HOL-Library.Conditional_Parametricity provides command
   6.432 +'parametric_constant' for proving parametricity of non-recursive
   6.433 +definitions. For constants that are not fully parametric the command
   6.434 +will infer conditions on relations (e.g., bi_unique, bi_total, or type
   6.435 +class conditions such as "respects 0") sufficient for parametricity. See
   6.436 +theory HOL-ex.Conditional_Parametricity_Examples for some examples.
   6.437 +
   6.438 +* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
   6.439 +generator to generate code for algebraic types with lazy evaluation
   6.440 +semantics even in call-by-value target languages. See theory
   6.441 +HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
   6.442 +
   6.443 +* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
   6.444 +
   6.445 +* Theory HOL-Library.Old_Datatype no longer provides the legacy command
   6.446 +'old_datatype'. INCOMPATIBILITY.
   6.447 +
   6.448 +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
   6.449 +instances of rat, real, complex as factorial rings etc. Import
   6.450 +HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
   6.451 +INCOMPATIBILITY.
   6.452 +
   6.453 +* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
   6.454 +infix/prefix notation.
   6.455 +
   6.456 +* Session HOL-Analysis: infinite products, Moebius functions, the
   6.457 +Riemann mapping theorem, the Vitali covering theorem,
   6.458 +change-of-variables results for integration and measures.
   6.459  
   6.460  
   6.461  *** ML ***
   6.462 @@ -371,47 +385,12 @@
   6.463  
   6.464  *** System ***
   6.465  
   6.466 -* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
   6.467 -heap images and session databases are always stored in
   6.468 -$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
   6.469 -$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
   6.470 -"isabelle jedit -s" or "isabelle build -s").
   6.471 -
   6.472 -* The command-line tool "export" and 'export_files' in session ROOT
   6.473 -entries retrieve theory exports from the session build database.
   6.474 -
   6.475 -* The command-line tools "isabelle server" and "isabelle client" provide
   6.476 -access to the Isabelle Server: it supports responsive session management
   6.477 -and concurrent use of theories, based on Isabelle/PIDE infrastructure.
   6.478 -See also the "system" manual.
   6.479 -
   6.480 -* The command-line tool "dump" dumps information from the cumulative
   6.481 -PIDE session database: many sessions may be loaded into a given logic
   6.482 -image, results from all loaded theories are written to the output
   6.483 -directory.
   6.484 -
   6.485 -* The command-line tool "isabelle update_comments" normalizes formal
   6.486 -comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
   6.487 -approximate the appearance in document output). This is more specific
   6.488 -than former "isabelle update_cartouches -c": the latter tool option has
   6.489 -been discontinued.
   6.490 -
   6.491 -* Session ROOT entry: empty 'document_files' means there is no document
   6.492 -for this session. There is no need to specify options [document = false]
   6.493 -anymore.
   6.494 -
   6.495 -* The command-line tool "isabelle mkroot" now always produces a document
   6.496 -outline: its options have been adapted accordingly. INCOMPATIBILITY.
   6.497 -
   6.498 -* The command-line tool "isabelle mkroot -I" initializes a Mercurial
   6.499 -repository for the generated session files.
   6.500 -
   6.501 -* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
   6.502 -support has been discontinued.
   6.503 -
   6.504  * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
   6.505  longer supported.
   6.506  
   6.507 +* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
   6.508 +support has been discontinued.
   6.509 +
   6.510  * Java runtime is for x86_64 only. Corresponding Isabelle settings have
   6.511  been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
   6.512  instead of former 32/64 variants. INCOMPATIBILITY.
   6.513 @@ -439,17 +418,46 @@
   6.514  corresponding environment values into account, when determining the
   6.515  up-to-date status of a session.
   6.516  
   6.517 +* The command-line tool "dump" dumps information from the cumulative
   6.518 +PIDE session database: many sessions may be loaded into a given logic
   6.519 +image, results from all loaded theories are written to the output
   6.520 +directory.
   6.521 +
   6.522  * Command-line tool "isabelle imports -I" also reports actual session
   6.523  imports. This helps to minimize the session dependency graph.
   6.524  
   6.525 -* Update to current Poly/ML 5.7.1 with slightly improved performance and
   6.526 -PIDE markup for identifier bindings.
   6.527 +* The command-line tool "export" and 'export_files' in session ROOT
   6.528 +entries retrieve theory exports from the session build database.
   6.529 +
   6.530 +* The command-line tools "isabelle server" and "isabelle client" provide
   6.531 +access to the Isabelle Server: it supports responsive session management
   6.532 +and concurrent use of theories, based on Isabelle/PIDE infrastructure.
   6.533 +See also the "system" manual.
   6.534 +
   6.535 +* The command-line tool "isabelle update_comments" normalizes formal
   6.536 +comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
   6.537 +approximate the appearance in document output). This is more specific
   6.538 +than former "isabelle update_cartouches -c": the latter tool option has
   6.539 +been discontinued.
   6.540 +
   6.541 +* The command-line tool "isabelle mkroot" now always produces a document
   6.542 +outline: its options have been adapted accordingly. INCOMPATIBILITY.
   6.543 +
   6.544 +* The command-line tool "isabelle mkroot -I" initializes a Mercurial
   6.545 +repository for the generated session files.
   6.546 +
   6.547 +* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
   6.548 +heap images and session databases are always stored in
   6.549 +$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
   6.550 +$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
   6.551 +"isabelle jedit -s" or "isabelle build -s").
   6.552  
   6.553  * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
   6.554  options for improved error reporting. Potential INCOMPATIBILITY with
   6.555  unusual LaTeX installations, may have to adapt these settings.
   6.556  
   6.557 -* The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision
   6.558 +* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
   6.559 +markup for identifier bindings. It now uses The GNU Multiple Precision
   6.560  Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
   6.561  32/64 bit.
   6.562  
     7.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Jun 06 13:04:52 2018 +0200
     7.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 06 14:23:13 2018 +0200
     7.3 @@ -305,7 +305,7 @@
     7.4  
     7.5    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
     7.6    different server name. The default server name is the official distribution
     7.7 -  name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
     7.8 +  name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the
     7.9    Isabelle desktop application without further options.
    7.10  
    7.11    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
     8.1 --- a/src/Doc/System/Environment.thy	Wed Jun 06 13:04:52 2018 +0200
     8.2 +++ b/src/Doc/System/Environment.thy	Wed Jun 06 14:23:13 2018 +0200
     8.3 @@ -58,7 +58,7 @@
     8.4      \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
     8.5      exists) is run in the same way as the site default settings. Note that the
     8.6      variable @{setting ISABELLE_HOME_USER} has already been set before ---
     8.7 -    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<close>.
     8.8 +    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2018\<close>.
     8.9  
    8.10      Thus individual users may override the site-wide defaults. Typically, a
    8.11      user settings file contains only a few lines, with some assignments that
    8.12 @@ -149,7 +149,7 @@
    8.13    of the @{executable isabelle} executable.
    8.14  
    8.15    \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
    8.16 -  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''.
    8.17 +  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018\<close>''.
    8.18  
    8.19    \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
    8.20    ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
     9.1 --- a/src/Doc/System/Misc.thy	Wed Jun 06 13:04:52 2018 +0200
     9.2 +++ b/src/Doc/System/Misc.thy	Wed Jun 06 14:23:13 2018 +0200
     9.3 @@ -220,7 +220,7 @@
     9.4  
     9.5    \<^medskip>
     9.6    The default is to output the full version string of the Isabelle
     9.7 -  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017: October 2017\<close>.
     9.8 +  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>.
     9.9  
    9.10    The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
    9.11    id of the @{setting ISABELLE_HOME} directory.
    10.1 --- a/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 13:04:52 2018 +0200
    10.2 +++ b/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 14:23:13 2018 +0200
    10.3 @@ -17,7 +17,7 @@
    10.4  text \<open>
    10.5    This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
    10.6  
    10.7 -  It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified
    10.8 +  It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
    10.9    set of type constructors lazily, even in target languages with eager evaluation.
   10.10    The lazy type must be algebraic, i.e., values must be built from constructors and a
   10.11    corresponding case operator decomposes them. Every datatype and codatatype is algebraic
    11.1 --- a/src/HOL/Parity.thy	Wed Jun 06 13:04:52 2018 +0200
    11.2 +++ b/src/HOL/Parity.thy	Wed Jun 06 14:23:13 2018 +0200
    11.3 @@ -933,7 +933,7 @@
    11.4  
    11.5  lemma drop_bit_of_nat:
    11.6    "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
    11.7 -	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
    11.8 +  by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
    11.9  
   11.10  end
   11.11  
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 13:04:52 2018 +0200
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:23:13 2018 +0200
    12.3 @@ -70,7 +70,7 @@
    12.4    apply (force simp add: linear_def real_scaleR_def[abs_def])
    12.5    done
    12.6  
    12.7 -hide_const (open)\<comment>\<open>locale constants\<close>
    12.8 +hide_const (open)\<comment> \<open>locale constants\<close>
    12.9    real_vector.dependent
   12.10    real_vector.independent
   12.11    real_vector.representation
   12.12 @@ -89,7 +89,7 @@
   12.13    unfolding linear_def real_scaleR_def
   12.14    by (rule refl)+
   12.15  
   12.16 -hide_const (open)\<comment>\<open>locale constants\<close>
   12.17 +hide_const (open)\<comment> \<open>locale constants\<close>
   12.18    real_vector.construct
   12.19  
   12.20  lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
   12.21 @@ -168,7 +168,7 @@
   12.22    apply (erule (1) nonzero_inverse_scaleR_distrib)
   12.23    done
   12.24  
   12.25 -lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment>\<open>legacy name\<close>
   12.26 +lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
   12.27  
   12.28  named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
   12.29  
    13.1 --- a/src/HOL/Vector_Spaces.thy	Wed Jun 06 13:04:52 2018 +0200
    13.2 +++ b/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:23:13 2018 +0200
    13.3 @@ -41,7 +41,7 @@
    13.4  
    13.5  locale vector_space =
    13.6    fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
    13.7 -  assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
    13.8 +  assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
    13.9     allows us to rewrite in the sublocale.\<close>
   13.10      "a *s (x + y) = a *s x + a *s y"
   13.11      "(a + b) *s x = a *s x + b *s x"
   13.12 @@ -68,7 +68,7 @@
   13.13  sublocale module scale rewrites "module_hom = linear"
   13.14    by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
   13.15  
   13.16 -lemmas\<comment>\<open>from \<open>module\<close>\<close>
   13.17 +lemmas\<comment> \<open>from \<open>module\<close>\<close>
   13.18        linear_id = module_hom_id
   13.19    and linear_ident = module_hom_ident
   13.20    and linear_scale_self = module_hom_scale_self
   13.21 @@ -607,7 +607,7 @@
   13.22  
   13.23  context fixes f assumes "linear s1 s2 f" begin
   13.24  interpretation linear s1 s2 f by fact
   13.25 -lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close>
   13.26 +lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
   13.27        linear_0 = zero
   13.28    and linear_add = add
   13.29    and linear_scale = scale
   13.30 @@ -634,7 +634,7 @@
   13.31    rewrites "module_hom = linear"
   13.32    by unfold_locales (fact module_hom_eq_linear)
   13.33  
   13.34 -lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close>
   13.35 +lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
   13.36        linear_eq_on_span = module_hom_eq_on_span
   13.37    and linear_compose_scale_right = module_hom_scale
   13.38    and linear_compose_add = module_hom_add
   13.39 @@ -834,7 +834,7 @@
   13.40    by (auto simp: that construct_in_span in_span_in_range_construct)
   13.41  
   13.42  lemma linear_independent_extend_subspace:
   13.43 -  \<comment>\<open>legacy: use @{term construct} instead\<close>
   13.44 +  \<comment> \<open>legacy: use @{term construct} instead\<close>
   13.45    assumes "vs1.independent B"
   13.46    shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)"
   13.47    by (rule exI[where x="construct B f"])
    14.1 --- a/src/Pure/General/cache.scala	Wed Jun 06 13:04:52 2018 +0200
    14.2 +++ b/src/Pure/General/cache.scala	Wed Jun 06 14:23:13 2018 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -/*  Title:      Pure/cache.scala
    14.5 +/*  Title:      Pure/General/cache.scala
    14.6      Author:     Makarius
    14.7  
    14.8  cache for partial sharing (weak table).
    15.1 --- a/src/Tools/jEdit/src-base/Isabelle_Base.props	Wed Jun 06 13:04:52 2018 +0200
    15.2 +++ b/src/Tools/jEdit/src-base/Isabelle_Base.props	Wed Jun 06 14:23:13 2018 +0200
    15.3 @@ -14,4 +14,4 @@
    15.4  
    15.5  #dependencies
    15.6  plugin.isabelle.jedit_base.Plugin.depend.0=jdk 1.8
    15.7 -plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.04.00.00
    15.8 +plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
    16.1 --- a/src/Tools/jEdit/src/Isabelle.props	Wed Jun 06 13:04:52 2018 +0200
    16.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Wed Jun 06 14:23:13 2018 +0200
    16.3 @@ -5,7 +5,7 @@
    16.4  #identification
    16.5  plugin.isabelle.jedit.Plugin.name=Isabelle
    16.6  plugin.isabelle.jedit.Plugin.author=Johannes Hlzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
    16.7 -plugin.isabelle.jedit.Plugin.version=9.0
    16.8 +plugin.isabelle.jedit.Plugin.version=10.0
    16.9  plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
   16.10  
   16.11  #system parameters
   16.12 @@ -14,7 +14,7 @@
   16.13  
   16.14  #dependencies
   16.15  plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
   16.16 -plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00
   16.17 +plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00
   16.18  plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
   16.19  plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
   16.20  plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8