# HG changeset patch # User wenzelm # Date 1528287793 -7200 # Node ID 194fa3d2d6a4d01f9f3cde59125c466c525216be # Parent 691c02d1699bedf4707ab9841d0c41057cf3b354# Parent cace81744c61ef2a68a5820acffbc0fc27d6e01d merged diff -r 691c02d1699b -r 194fa3d2d6a4 ANNOUNCE --- 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 diff -r 691c02d1699b -r 194fa3d2d6a4 Admin/components/components.sha1 --- 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 diff -r 691c02d1699b -r 194fa3d2d6a4 Admin/components/main --- 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 diff -r 691c02d1699b -r 194fa3d2d6a4 CONTRIBUTORS --- 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 ----------------------------- diff -r 691c02d1699b -r 194fa3d2d6a4 COPYRIGHT --- 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. diff -r 691c02d1699b -r 194fa3d2d6a4 NEWS --- 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 "\ \text\", 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 "\" 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 "\" 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>\argument\. 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. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\". + * 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>\argument\. 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. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\". - -* 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 \ A . f Y \ 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 \ A . f Y \ 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\A. B and even MIN x. B (only useful for finite types), also -MAX. +MIN x\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 "\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: \ \text\ (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: \ \text\ (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. diff -r 691c02d1699b -r 194fa3d2d6a4 src/Doc/JEdit/JEdit.thy --- 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>\-n\ option reports the server name, and the \<^verbatim>\-s\ option provides a different server name. The default server name is the official distribution - name (e.g.\ \<^verbatim>\Isabelle2017\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2018\). Thus @{tool jedit_client} can connect to the Isabelle desktop application without further options. The \<^verbatim>\-p\ option allows to override the implicit default of the system diff -r 691c02d1699b -r 194fa3d2d6a4 src/Doc/System/Environment.thy --- 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>\$USER_HOME/.isabelle/Isabelle2017\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2018\. 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}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2017\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2018\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r 691c02d1699b -r 194fa3d2d6a4 src/Doc/System/Misc.thy --- 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>\Isabelle2017: October 2017\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2018: August 2018\. The \<^verbatim>\-i\ option produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory. diff -r 691c02d1699b -r 194fa3d2d6a4 src/HOL/Library/Code_Lazy.thy --- 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 \ 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 diff -r 691c02d1699b -r 194fa3d2d6a4 src/HOL/Parity.thy --- 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 diff -r 691c02d1699b -r 194fa3d2d6a4 src/HOL/Real_Vector_Spaces.thy --- 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)\\locale constants\ +hide_const (open)\ \locale constants\ 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)\\locale constants\ +hide_const (open)\ \locale constants\ real_vector.construct lemma linear_compose: "linear f \ linear g \ 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\\legacy name\ +lemmas sum_constant_scaleR = real_vector.sum_constant_scale\ \legacy name\ named_theorems vector_add_divide_simps "to simplify sums of scaled vectors" diff -r 691c02d1699b -r 194fa3d2d6a4 src/HOL/Vector_Spaces.thy --- 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 \ 'b::ab_group_add \ 'b" (infixr "*s" 75) - assumes vector_space_assms:\\re-stating the assumptions of \module\ instead of extending \module\ + assumes vector_space_assms:\ \re-stating the assumptions of \module\ instead of extending \module\ allows us to rewrite in the sublocale.\ "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\\from \module\\ +lemmas\ \from \module\\ 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\\from locale \module_hom\\ +lemmas\ \from locale \module_hom\\ 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\\from locale \module_pair\\ +lemmas\ \from locale \module_pair\\ 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: - \\legacy: use @{term construct} instead\ + \ \legacy: use @{term construct} instead\ assumes "vs1.independent B" shows "\g. linear s1 s2 g \ (\x\B. g x = f x) \ range g = vs2.span (f`B)" by (rule exI[where x="construct B f"]) diff -r 691c02d1699b -r 194fa3d2d6a4 src/Pure/General/cache.scala --- 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). diff -r 691c02d1699b -r 194fa3d2d6a4 src/Tools/jEdit/src-base/Isabelle_Base.props --- 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 diff -r 691c02d1699b -r 194fa3d2d6a4 src/Tools/jEdit/src/Isabelle.props --- 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