merged
authorwenzelm
Wed, 06 Jun 2018 14:23:13 +0200
changeset 68398 194fa3d2d6a4
parent 68387 691c02d1699b (current diff)
parent 68397 cace81744c61 (diff)
child 68400 cada19e0c6c7
child 68401 cd53ad6e7d96
merged
--- a/ANNOUNCE	Wed Jun 06 13:04:52 2018 +0200
+++ b/ANNOUNCE	Wed Jun 06 14:23:13 2018 +0200
@@ -1,32 +1,15 @@
-Subject: Announcing Isabelle2017
+Subject: Announcing Isabelle2018
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2017 is now available.
+Isabelle2018 is now available.
 
-This version introduces many changes over Isabelle2016-1: see the NEWS
+This version introduces many changes over Isabelle2017: see the NEWS
 file for further details. Some notable points:
 
-* Experimental support for Visual Studio Code as alternative PIDE front-end.
-
-* Improved Isabelle/jEdit Prover IDE: management of session sources
-independently of editor buffers, removal of unused theories, explicit
-indication of theory status, more careful auto-indentation.
-
-* Session-qualified theory imports.
-
-* Code generator improvements: support for statically embedded computations.
-
-* Numerous HOL library improvements.
-
-* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
-(ported from HOL-Light).
-
-* Improved Nunchaku model finder, now in main HOL.
-
-* SQL database support in Isabelle/Scala.
+* FIXME.
 
 
-You may get Isabelle2017 from the following mirror sites:
+You may get Isabelle2018 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle
   Munich (Germany)     http://isabelle.in.tum.de
--- a/Admin/components/components.sha1	Wed Jun 06 13:04:52 2018 +0200
+++ b/Admin/components/components.sha1	Wed Jun 06 14:23:13 2018 +0200
@@ -215,6 +215,7 @@
 b016a785f1f78855c00d351ff598355c3b87450f  sqlite-jdbc-3.18.0-1.tar.gz
 b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf  sqlite-jdbc-3.18.0.tar.gz
 e56117a67ab01fb24c7fc054ede3160cefdac5f8  sqlite-jdbc-3.20.0.tar.gz
+27aeac6a91353d69f0438837798ac4ae6f9ff8c5  sqlite-jdbc-3.23.1.tar.gz
 8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
 2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
--- a/Admin/components/main	Wed Jun 06 13:04:52 2018 +0200
+++ b/Admin/components/main	Wed Jun 06 14:23:13 2018 +0200
@@ -17,7 +17,7 @@
 smbc-0.4.1
 ssh-java-20161009
 spass-3.8ds-1
-sqlite-jdbc-3.20.0
+sqlite-jdbc-3.23.1
 verit-2016post
 xz-java-1.8
 z3-4.4.0pre-2
--- a/CONTRIBUTORS	Wed Jun 06 13:04:52 2018 +0200
+++ b/CONTRIBUTORS	Wed Jun 06 14:23:13 2018 +0200
@@ -3,11 +3,11 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2018
+-----------------------------
 
 * May 2018: Manuel Eberl
-  Landau symbols and asymptotic equivalence (moved from the AFP)
+  Landau symbols and asymptotic equivalence (moved from the AFP).
 
 * May 2018: Jose Divasón (Universidad de la Rioja),
   Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
@@ -22,9 +22,8 @@
   Code generation with lazy evaluation semantics.
 
 * March 2018: Florian Haftmann
-  Abstract bit operations push_bit, take_bit, drop_bit, alongside
-  with an algebraic foundation for bit strings and word types in
-  HOL-ex.
+  Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
+  algebraic foundation for bit strings and word types in HOL-ex.
 
 * March 2018: Viorel Preoteasa
   Generalisation of complete_distrib_lattice
@@ -36,7 +35,8 @@
   A new conditional parametricity prover.
 
 * October 2017: Alexander Maletzky
-  Derivation of axiom "iff" in HOL.thy from the other axioms.
+  Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
+
 
 Contributions to Isabelle2017
 -----------------------------
--- a/COPYRIGHT	Wed Jun 06 13:04:52 2018 +0200
+++ b/COPYRIGHT	Wed Jun 06 14:23:13 2018 +0200
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 1986-2017,
+Copyright (c) 1986-2018,
   University of Cambridge,
   Technische Universitaet Muenchen,
   and contributors.
--- a/NEWS	Wed Jun 06 13:04:52 2018 +0200
+++ b/NEWS	Wed Jun 06 14:23:13 2018 +0200
@@ -4,11 +4,21 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2018 (August 2018)
+---------------------------------
 
 *** General ***
 
+* Session-qualified theory names are mandatory: it is no longer possible
+to refer to unqualified theories from the parent session.
+INCOMPATIBILITY for old developments that have not been updated to
+Isabelle2017 yet (using the "isabelle imports" tool).
+
+* Only the most fundamental theory names are global, usually the entry
+points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
+FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
+formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
+
 * Marginal comments need to be written exclusively in the new-style form
 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
 supported. INCOMPATIBILITY, use the command-line tool "isabelle
@@ -29,23 +39,9 @@
 In case you want to exclude conversion of ML files (because the tool
 frequently also converts ML's "op" syntax), use option "-m".
 
-* The old 'def' command has been discontinued (legacy since
-Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
-object-logic equality or equivalence.
-
-* Session-qualified theory names are mandatory: it is no longer possible
-to refer to unqualified theories from the parent session.
-INCOMPATIBILITY for old developments that have not been updated to
-Isabelle2017 yet (using the "isabelle imports" tool).
-
 * Theory header 'abbrevs' specifications need to be separated by 'and'.
 INCOMPATIBILITY.
 
-* Only the most fundamental theory names are global, usually the entry
-points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
-FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
-formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
-
 * Command 'external_file' declares the formal dependency on the given
 file name, such that the Isabelle build process knows about it, but
 without specific Prover IDE management.
@@ -64,13 +60,45 @@
 * The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
 use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
 
-* Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to
-avoid unclear meaning of the old "soft hyphen" U+00AD. Rare
-INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.
+* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit
+Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
+U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
+output.
 
 
 *** Isabelle/jEdit Prover IDE ***
 
+* The command-line tool "isabelle jedit" provides more flexible options
+for session management:
+
+  - option -R builds an auxiliary logic image with all required theories
+    from other sessions, relative to an ancestor session given by option
+    -A (default: parent)
+
+  - option -S is like -R, with a focus on the selected session and its
+    descendants (this reduces startup time for big projects like AFP)
+
+  Examples:
+    isabelle jedit -R HOL-Number_Theory
+    isabelle jedit -R HOL-Number_Theory -A HOL
+    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
+    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
+
+* PIDE markup for session ROOT files: allows to complete session names,
+follow links to theories and document files etc.
+
+* Completion supports theory header imports, using theory base name.
+E.g. "Prob" may be completed to "HOL-Probability.Probability".
+
+* Named control symbols (without special Unicode rendering) are shown as
+bold-italic keyword. This is particularly useful for the short form of
+antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
+"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
+arguments into this format.
+
+* Completion provides templates for named symbols with arguments,
+e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
+
 * Slightly more parallel checking, notably for high priority print
 functions (e.g. State output).
 
@@ -82,37 +110,6 @@
 supersede former "spell_checker_elements" to determine regions of text
 that are subject to spell-checking. Minor INCOMPATIBILITY.
 
-* PIDE markup for session ROOT files: allows to complete session names,
-follow links to theories and document files etc.
-
-* Completion supports theory header imports, using theory base name.
-E.g. "Prob" may be completed to "HOL-Probability.Probability".
-
-* The command-line tool "isabelle jedit" provides more flexible options
-for session management:
-  - option -R builds an auxiliary logic image with all required theories
-    from other sessions, relative to an ancestor session given by option
-    -A (default: parent)
-  - option -S is like -R, with a focus on the selected session and its
-    descendants (this reduces startup time for big projects like AFP)
-
-  Examples:
-    isabelle jedit -R HOL-Number_Theory
-    isabelle jedit -R HOL-Number_Theory -A HOL
-    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
-    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
-
-* Named control symbols (without special Unicode rendering) are shown as
-bold-italic keyword. This is particularly useful for the short form of
-antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
-"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
-arguments into this format.
-
-* Completion provides templates for named symbols with arguments,
-e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
-
-* Bibtex database files (.bib) are semantically checked.
-
 * Action "isabelle.preview" is able to present more file formats,
 notably bibtex database files and ML files.
 
@@ -120,6 +117,8 @@
 plain-text document draft. Both are available via the menu "Plugins /
 Isabelle".
 
+* Bibtex database files (.bib) are semantically checked.
+
 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
 is only used if there is no conflict with existing Unicode sequences in
 the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
@@ -163,19 +162,23 @@
 antiquotations in control symbol notation, e.g. \<^const_name> becomes
 \isactrlconstUNDERSCOREname.
 
-* Document antiquotation @{cite} now checks the given Bibtex entries
-against the Bibtex database files -- only in batch-mode session builds.
+* Document preparation with skip_proofs option now preserves the content
+more accurately: only terminal proof steps ('by' etc.) are skipped.
 
 * Document antiquotation @{session name} checks and prints the given
 session name verbatim.
 
-* Document preparation with skip_proofs option now preserves the content
-more accurately: only terminal proof steps ('by' etc.) are skipped.
+* Document antiquotation @{cite} now checks the given Bibtex entries
+against the Bibtex database files -- only in batch-mode session builds.
 
 * Command-line tool "isabelle document" has been re-implemented in
 Isabelle/Scala, with simplified arguments and explicit errors from the
 latex and bibtex process. Minor INCOMPATIBILITY.
 
+* Session ROOT entry: empty 'document_files' means there is no document
+for this session. There is no need to specify options [document = false]
+anymore.
+
 
 *** Isar ***
 
@@ -185,13 +188,17 @@
 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
 (e.g. use 'find_theorems' or 'try' to figure this out).
 
+* The old 'def' command has been discontinued (legacy since
+Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
+object-logic equality or equivalence.
+
 * Rewrites clauses (keyword 'rewrites') were moved into the locale
-expression syntax, where they are part of locale instances.  In
-interpretation commands rewrites clauses now need to occur before
-'for' and 'defines'.  Minor INCOMPATIBILITY.
-
-* For rewrites clauses, if activating a locale instance fails, fall
-back to reading the clause first.  This helps avoid qualification of
+expression syntax, where they are part of locale instances. In
+interpretation commands rewrites clauses now need to occur before 'for'
+and 'defines'. Minor INCOMPATIBILITY.
+
+* For 'rewrites' clauses, if activating a locale instance fails, fall
+back to reading the clause first. This helps avoid qualification of
 locale instances where the qualifier's sole purpose is avoiding
 duplicate constant declarations.
 
@@ -204,54 +211,55 @@
 
 *** HOL ***
 
-* Landau_Symbols from the AFP was moved to HOL-Library
-
 * Clarified relationship of characters, strings and code generation:
 
-  * Type "char" is now a proper datatype of 8-bit values.
-
-  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
-    general conversions "of_char" and "char_of" with suitable
-    type constraints instead.
-
-  * The zero character is just written "CHR 0x00", not
-    "0" any longer.
-
-  * Type "String.literal" (for code generation) is now isomorphic
-    to lists of 7-bit (ASCII) values; concrete values can be written
-    as "STR ''...''" for sequences of printable characters and
-    "STR 0x..." for one single ASCII code point given
-    as hexadecimal numeral.
-
-  * Type "String.literal" supports concatenation "... + ..."
-    for all standard target languages.
-
-  * Theory Library/Code_Char is gone; study the explanations concerning
-    "String.literal" in the tutorial on code generation to get an idea
-    how target-language string literals can be converted to HOL string
-    values and vice versa.
-
-  * Imperative-HOL: operation "raise" directly takes a value of type
-    "String.literal" as argument, not type "string".
-
-INCOMPATIBILITY.
-
-* Abstract bit operations as part of Main: push_bit, take_bit,
-drop_bit.
-
-* New, more general, axiomatization of complete_distrib_lattice.
-The former axioms:
-"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
-are replaced by
-"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
-The instantiations of sets and functions as complete_distrib_lattice
-are moved to Hilbert_Choice.thy because their proofs need the Hilbert
-choice operator. The dual of this property is also proved in
-Hilbert_Choice.thy.
+  - Type "char" is now a proper datatype of 8-bit values.
+
+  - Conversions "nat_of_char" and "char_of_nat" are gone; use more
+    general conversions "of_char" and "char_of" with suitable type
+    constraints instead.
+
+  - The zero character is just written "CHR 0x00", not "0" any longer.
+
+  - Type "String.literal" (for code generation) is now isomorphic to
+    lists of 7-bit (ASCII) values; concrete values can be written as
+    "STR ''...''" for sequences of printable characters and "STR 0x..."
+    for one single ASCII code point given as hexadecimal numeral.
+
+  - Type "String.literal" supports concatenation "... + ..." for all
+    standard target languages.
+
+  - Theory HOL-Library.Code_Char is gone; study the explanations
+    concerning "String.literal" in the tutorial on code generation to
+    get an idea how target-language string literals can be converted to
+    HOL string values and vice versa.
+
+  - Session Imperative-HOL: operation "raise" directly takes a value of
+    type "String.literal" as argument, not type "string".
+
+INCOMPATIBILITY.
+
+* Code generation: Code generation takes an explicit option
+"case_insensitive" to accomodate case-insensitive file systems.
+
+* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
+
+* New, more general, axiomatization of complete_distrib_lattice. The
+former axioms:
+
+  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
+
+are replaced by:
+
+  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
+
+The instantiations of sets and functions as complete_distrib_lattice are
+moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
+operator. The dual of this property is also proved in theory
+HOL.Hilbert_Choice.
 
 * New syntax for the minimum/maximum of a function over a finite set:
-MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
-MAX.
+MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.
 
 * Clarifed theorem names:
 
@@ -260,83 +268,59 @@
 
 Minor INCOMPATIBILITY.
 
-* A new command parametric_constant for proving parametricity of
-non-recursive definitions. For constants that are not fully parametric
-the command will infer conditions on relations (e.g., bi_unique,
-bi_total, or type class conditions such as "respects 0") sufficient for
-parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
-some examples.
-
-* A new preprocessor for the code generator to generate code for algebraic
-  types with lazy evaluation semantics even in call-by-value target languages.
-  See theory HOL-Library.Code_Lazy for the implementation and
-  HOL-Codegenerator_Test.Code_Lazy_Test for examples.
-
 * SMT module:
+
   - The 'smt_oracle' option is now necessary when using the 'smt' method
     with a solver other than Z3. INCOMPATIBILITY.
+
   - The encoding to first-order logic is now more complete in the
     presence of higher-order quantifiers. An 'smt_explicit_application'
     option has been added to control this. INCOMPATIBILITY.
 
-* Datatypes:
-  - The legacy command 'old_datatype', provided by
-    '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
-
-* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
-instances of rat, real, complex as factorial rings etc. Import
-HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
-INCOMPATIBILITY.
-
 * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
 sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
 interpretation of abstract locales. INCOMPATIBILITY.
 
+* Predicate coprime is now a real definition, not a mere abbreviation.
+INCOMPATIBILITY.
+
 * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
 INCOMPATIBILITY.
 
 * The relator rel_filter on filters has been strengthened to its
-canonical categorical definition with better properties. INCOMPATIBILITY.
+canonical categorical definition with better properties.
+INCOMPATIBILITY.
 
 * Generalized linear algebra involving linear, span, dependent, dim
 from type class real_vector to locales module and vector_space.
 Renamed:
-  - span_inc ~> span_superset
-  - span_superset ~> span_base
-  - span_eq ~> span_eq_iff
-INCOMPATIBILITY.
-
-* HOL-Algebra: renamed (^) to [^]
-
-* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
-theorem, the Vitali covering theorem, change-of-variables results for
-integration and measures.
+
+  span_inc ~> span_superset
+  span_superset ~> span_base
+  span_eq ~> span_eq_iff
+
+INCOMPATIBILITY.
 
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
 
-* Theory List: functions "sorted_wrt" and "sorted" now compare every
-  element in a list to all following elements, not just the next one.
-
-* Theory List: Synatx:
-  - filter-syntax "[x <- xs. P]" is no longer output syntax
-    but only input syntax.
-  - list comprehension syntax now supports tuple patterns in "pat <- xs".
+* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
+element in a list to all following elements, not just the next one.
+
+* Theory HOL.List syntax:
+
+  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only
+    input syntax
+
+  - list comprehension syntax now supports tuple patterns in "pat <- xs"
 
 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
 
-* Predicate coprime is now a real definition, not a mere
-abbreviation. INCOMPATIBILITY.
-
-* Code generation: Code generation takes an explicit option
-"case_insensitive" to accomodate case-insensitive file systems.
-
 * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
 clash with fact mod_mult_self4 (on more generic semirings).
 INCOMPATIBILITY.
 
 * Eliminated some theorem aliasses:
-
   even_times_iff ~> even_mult_iff
   mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
   even_of_nat ~> even_int_iff
@@ -344,18 +328,48 @@
 INCOMPATIBILITY.
 
 * Eliminated some theorem duplicate variations:
-  * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
-  * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
-  * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
-  * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
-  * The witness of mod_eqD can be given directly as "_ div _".
+
+  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
+  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc
+  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
+  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
+  - the witness of mod_eqD can be given directly as "_ div _"
 
 INCOMPATIBILITY.
 
 * Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
-longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
-adding "elim!: dvd" to classical proof methods in most situations
-restores broken proofs.
+longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding
+"elim!: dvd" to classical proof methods in most situations restores
+broken proofs.
+
+* Theory HOL-Library.Conditional_Parametricity provides command
+'parametric_constant' for proving parametricity of non-recursive
+definitions. For constants that are not fully parametric the command
+will infer conditions on relations (e.g., bi_unique, bi_total, or type
+class conditions such as "respects 0") sufficient for parametricity. See
+theory HOL-ex.Conditional_Parametricity_Examples for some examples.
+
+* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
+generator to generate code for algebraic types with lazy evaluation
+semantics even in call-by-value target languages. See theory
+HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
+
+* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
+
+* Theory HOL-Library.Old_Datatype no longer provides the legacy command
+'old_datatype'. INCOMPATIBILITY.
+
+* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
+instances of rat, real, complex as factorial rings etc. Import
+HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
+INCOMPATIBILITY.
+
+* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
+infix/prefix notation.
+
+* Session HOL-Analysis: infinite products, Moebius functions, the
+Riemann mapping theorem, the Vitali covering theorem,
+change-of-variables results for integration and measures.
 
 
 *** ML ***
@@ -371,47 +385,12 @@
 
 *** System ***
 
-* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
-heap images and session databases are always stored in
-$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
-$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
-"isabelle jedit -s" or "isabelle build -s").
-
-* The command-line tool "export" and 'export_files' in session ROOT
-entries retrieve theory exports from the session build database.
-
-* The command-line tools "isabelle server" and "isabelle client" provide
-access to the Isabelle Server: it supports responsive session management
-and concurrent use of theories, based on Isabelle/PIDE infrastructure.
-See also the "system" manual.
-
-* The command-line tool "dump" dumps information from the cumulative
-PIDE session database: many sessions may be loaded into a given logic
-image, results from all loaded theories are written to the output
-directory.
-
-* The command-line tool "isabelle update_comments" normalizes formal
-comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
-approximate the appearance in document output). This is more specific
-than former "isabelle update_cartouches -c": the latter tool option has
-been discontinued.
-
-* Session ROOT entry: empty 'document_files' means there is no document
-for this session. There is no need to specify options [document = false]
-anymore.
-
-* The command-line tool "isabelle mkroot" now always produces a document
-outline: its options have been adapted accordingly. INCOMPATIBILITY.
-
-* The command-line tool "isabelle mkroot -I" initializes a Mercurial
-repository for the generated session files.
-
-* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
-support has been discontinued.
-
 * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
 longer supported.
 
+* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
+support has been discontinued.
+
 * Java runtime is for x86_64 only. Corresponding Isabelle settings have
 been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
 instead of former 32/64 variants. INCOMPATIBILITY.
@@ -439,17 +418,46 @@
 corresponding environment values into account, when determining the
 up-to-date status of a session.
 
+* The command-line tool "dump" dumps information from the cumulative
+PIDE session database: many sessions may be loaded into a given logic
+image, results from all loaded theories are written to the output
+directory.
+
 * Command-line tool "isabelle imports -I" also reports actual session
 imports. This helps to minimize the session dependency graph.
 
-* Update to current Poly/ML 5.7.1 with slightly improved performance and
-PIDE markup for identifier bindings.
+* The command-line tool "export" and 'export_files' in session ROOT
+entries retrieve theory exports from the session build database.
+
+* The command-line tools "isabelle server" and "isabelle client" provide
+access to the Isabelle Server: it supports responsive session management
+and concurrent use of theories, based on Isabelle/PIDE infrastructure.
+See also the "system" manual.
+
+* The command-line tool "isabelle update_comments" normalizes formal
+comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
+approximate the appearance in document output). This is more specific
+than former "isabelle update_cartouches -c": the latter tool option has
+been discontinued.
+
+* The command-line tool "isabelle mkroot" now always produces a document
+outline: its options have been adapted accordingly. INCOMPATIBILITY.
+
+* The command-line tool "isabelle mkroot -I" initializes a Mercurial
+repository for the generated session files.
+
+* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
+heap images and session databases are always stored in
+$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
+$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
+"isabelle jedit -s" or "isabelle build -s").
 
 * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
 options for improved error reporting. Potential INCOMPATIBILITY with
 unusual LaTeX installations, may have to adapt these settings.
 
-* The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision
+* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
+markup for identifier bindings. It now uses The GNU Multiple Precision
 Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
 32/64 bit.
 
--- a/src/Doc/JEdit/JEdit.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -305,7 +305,7 @@
 
   The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   different server name. The default server name is the official distribution
-  name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
+  name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the
   Isabelle desktop application without further options.
 
   The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
--- a/src/Doc/System/Environment.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Doc/System/Environment.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -58,7 +58,7 @@
     \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
     exists) is run in the same way as the site default settings. Note that the
     variable @{setting ISABELLE_HOME_USER} has already been set before ---
-    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<close>.
+    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2018\<close>.
 
     Thus individual users may override the site-wide defaults. Typically, a
     user settings file contains only a few lines, with some assignments that
@@ -149,7 +149,7 @@
   of the @{executable isabelle} executable.
 
   \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
-  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''.
+  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018\<close>''.
 
   \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
   ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Doc/System/Misc.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -220,7 +220,7 @@
 
   \<^medskip>
   The default is to output the full version string of the Isabelle
-  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017: October 2017\<close>.
+  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>.
 
   The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
   id of the @{setting ISABELLE_HOME} directory.
--- a/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -17,7 +17,7 @@
 text \<open>
   This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
 
-  It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified
+  It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
   set of type constructors lazily, even in target languages with eager evaluation.
   The lazy type must be algebraic, i.e., values must be built from constructors and a
   corresponding case operator decomposes them. Every datatype and codatatype is algebraic
--- a/src/HOL/Parity.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Parity.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -933,7 +933,7 @@
 
 lemma drop_bit_of_nat:
   "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
-	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+  by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
 
 end
 
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -70,7 +70,7 @@
   apply (force simp add: linear_def real_scaleR_def[abs_def])
   done
 
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
   real_vector.dependent
   real_vector.independent
   real_vector.representation
@@ -89,7 +89,7 @@
   unfolding linear_def real_scaleR_def
   by (rule refl)+
 
-hide_const (open)\<comment>\<open>locale constants\<close>
+hide_const (open)\<comment> \<open>locale constants\<close>
   real_vector.construct
 
 lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
@@ -168,7 +168,7 @@
   apply (erule (1) nonzero_inverse_scaleR_distrib)
   done
 
-lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment>\<open>legacy name\<close>
+lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
 
 named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
 
--- a/src/HOL/Vector_Spaces.thy	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Wed Jun 06 14:23:13 2018 +0200
@@ -41,7 +41,7 @@
 
 locale vector_space =
   fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
-  assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
+  assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
    allows us to rewrite in the sublocale.\<close>
     "a *s (x + y) = a *s x + a *s y"
     "(a + b) *s x = a *s x + b *s x"
@@ -68,7 +68,7 @@
 sublocale module scale rewrites "module_hom = linear"
   by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
 
-lemmas\<comment>\<open>from \<open>module\<close>\<close>
+lemmas\<comment> \<open>from \<open>module\<close>\<close>
       linear_id = module_hom_id
   and linear_ident = module_hom_ident
   and linear_scale_self = module_hom_scale_self
@@ -607,7 +607,7 @@
 
 context fixes f assumes "linear s1 s2 f" begin
 interpretation linear s1 s2 f by fact
-lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
       linear_0 = zero
   and linear_add = add
   and linear_scale = scale
@@ -634,7 +634,7 @@
   rewrites "module_hom = linear"
   by unfold_locales (fact module_hom_eq_linear)
 
-lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close>
+lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
       linear_eq_on_span = module_hom_eq_on_span
   and linear_compose_scale_right = module_hom_scale
   and linear_compose_add = module_hom_add
@@ -834,7 +834,7 @@
   by (auto simp: that construct_in_span in_span_in_range_construct)
 
 lemma linear_independent_extend_subspace:
-  \<comment>\<open>legacy: use @{term construct} instead\<close>
+  \<comment> \<open>legacy: use @{term construct} instead\<close>
   assumes "vs1.independent B"
   shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)"
   by (rule exI[where x="construct B f"])
--- a/src/Pure/General/cache.scala	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Pure/General/cache.scala	Wed Jun 06 14:23:13 2018 +0200
@@ -1,4 +1,4 @@
-/*  Title:      Pure/cache.scala
+/*  Title:      Pure/General/cache.scala
     Author:     Makarius
 
 cache for partial sharing (weak table).
--- a/src/Tools/jEdit/src-base/Isabelle_Base.props	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Tools/jEdit/src-base/Isabelle_Base.props	Wed Jun 06 14:23:13 2018 +0200
@@ -14,4 +14,4 @@
 
 #dependencies
 plugin.isabelle.jedit_base.Plugin.depend.0=jdk 1.8
-plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.04.00.00
+plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
--- a/src/Tools/jEdit/src/Isabelle.props	Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Wed Jun 06 14:23:13 2018 +0200
@@ -5,7 +5,7 @@
 #identification
 plugin.isabelle.jedit.Plugin.name=Isabelle
 plugin.isabelle.jedit.Plugin.author=Johannes Hlzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=9.0
+plugin.isabelle.jedit.Plugin.version=10.0
 plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
 
 #system parameters
@@ -14,7 +14,7 @@
 
 #dependencies
 plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
-plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00
+plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00
 plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
 plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
 plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8