--- 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 Hölzl, 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