NEWS

proper NEWS;

Isabelle NEWS -- history of user-relevant changes
=================================================

(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)


New in this Isabelle version
----------------------------

*** General ***

* Commands 'syntax' and 'no_syntax' now work in a local theory context,
but there is no proper way to refer to local entities --- in contrast to
'notation' and 'no_notation'. Local syntax works well with 'bundle',
e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
Isabelle/HOL.

* Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
in interactive mode, but it could occasionally cause unnecessary
slowdown. It can be disabled like this:

  context notes [[show_results = false]]
  begin
    definition "test = True"
    theorem test by (simp add: test_def)
  end

* Timeouts for Isabelle/ML tools are subject to system option
"timeout_scale" --- this already used for the overall session build
process before, and allows to adapt to slow machines. The underlying
Timeout.apply in Isabelle/ML treats an original timeout specification 0
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
in boundary cases.

* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
managed via Isabelle/Scala instead of perl; the dependency on
libwww-perl has been eliminated (notably on Linux). Rare
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html

* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.


*** Isabelle/jEdit Prover IDE ***

* More robust 'proof' outline for method "induct": support nested cases.

* Support for built-in font substitution of jEdit text area.

* The main plugin for Isabelle/jEdit can be deactivated and reactivated
as documented --- was broken at least since Isabelle2018.


*** Document preparation ***

* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
"pifont").

* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.

* Document antiquotations for ML text have been refined: "def" and "ref"
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
type arguments for constructors (only relevant for index), e.g.
@{ML_type \<open>'a list\<close>} vs. @{ML_type 'a \<open>list\<close>}; @{ML_op} has been renamed
to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax.

* Option "document_logo" determines if an instance of the Isabelle logo
should be created in the document output directory. The given string
specifies the name of the logo variant, while "_" (underscore) refers to
the unnamed variant. The output file name is always "isabelle_logo.pdf".

* Option "document_preprocessor" specifies the name of an executable
that is run within the document output directory, after preparing the
document sources and before the actual build process. This allows to
apply adhoc patches, without requiring a separate "build" script.

* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:

  - "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
    build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX

  - "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
    special LaTeX styles)

  - "build": delegate to the executable "./build pdf"

The presence of a "build" command within the document output directory
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.

* The command-line tool "isabelle latex" has been discontinued,
INCOMPATIBILITY for old document build scripts.

  - Former "isabelle latex -o sty" has become obsolete: Isabelle .sty
    files are automatically generated within the document output
    directory.

  - Former "isabelle latex -o pdf" should be replaced by
    "$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without
    quotes), according to the intended LaTeX engine.

  - Former "isabelle latex -o bbl" should be replaced by
    "$ISABELLE_BIBTEX root" (without quotes).

  - Former "isabelle latex -o idx" should be replaced by
    "$ISABELLE_MAKEINDEX root" (without quotes).

* Option "document_bibliography" explicitly enables the use of bibtex;
the default is to check the presence of root.bib, but it could have a
different name.

* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").

* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
no longer required.


*** Pure ***

* "global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
"global_interpretation".


*** HOL ***

* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in
a global theory via 'unbundle'. The opposite declarations are bundled as
"no_lattice_syntax". Minor INCOMPATIBILITY.

* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
use explict expression instead. Minor INCOMPATIBILITY.

* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
Melem, not_Melem to empty_mset, member_mset, not_member_mset
respectively. Minor INCOMPATIBILITY.

* Theory "HOL-Library.Multiset": consolidated operation and fact names:
    inf_subset_mset ~> inter_mset
    sup_subset_mset ~> union_mset
    multiset_inter_def ~> inter_mset_def
    sup_subset_mset_def ~> union_mset_def
    multiset_inter_count ~> count_inter_mset
    sup_subset_mset_count ~> count_union_mset

* Theory "HOL-Library.Multiset": syntax precendence for membership
operations has been adjusted to match the corresponding precendences on
sets. Rare INCOMPATIBILITY.

* Theory "HOL-Library.Cardinality": code generator setup based on the
type classes finite_UNIV and card_UNIV has been moved to
"HOL-Library.Code_Cardinality", to avoid incompatibilities with
other code setups for sets in AFP/Containers. Applications relying on
this code setup should import "HOL-Library.Code_Cardinality". Minor
INCOMPATIBILITY.

* Session "HOL-Analysis" and "HOL-Probability": indexed products of
discrete distributions, negative binomial distribution, Hoeffding's
inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
and some more small lemmas. Some theorems that were stated awkwardly
before were corrected. Minor INCOMPATIBILITY.

* Session "HOL-Analysis": the complex Arg function has been identified
with the function "arg" of Complex_Main, renaming arg->Arg also in the
names of arg_bounded. Minor INCOMPATIBILITY.

* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
potential for change can be avoided if interpretations of type class
"order" are replaced or augmented by interpretations of locale
"ordering".

* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
INCOMPATIBILITY; note that for most applications less elementary lemmas
exists.

* Theory "HOL-Library.Permutation" has been renamed to the more specific
"HOL-Library.List_Permutation". Note that most notions from that theory
are already present in theory "HOL-Combinatorics.Permutations".
INCOMPATIBILITY.

* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
"Multiset_Permutations", "Perm" have been moved there from session
HOL-Library.

* Theory "HOL-Combinatorics.Transposition" provides elementary swap
operation "transpose".

* Lemma "permutes_induct" has been given stronger hypotheses and named
premises. INCOMPATIBILITY.

* Combinator "Fun.swap" resolved into a mere input abbreviation in
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.

* Infix syntax for bit operations AND, OR, XOR is now organized in
bundle bit_operations_syntax. INCOMPATIBILITY.

* Bit operations set_bit, unset_bit and flip_bit are now class
operations. INCOMPATIBILITY.

* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.

* Simplified class hierarchy for bit operations: bit operations reside
in classes (semi)ring_bit_operations, class semiring_bit_shifts is
gone.

* Expressions of the form "NOT (numeral _)" are not simplified by
default any longer.  INCOMPATIBILITY, use not_one_eq and not_numeral_eq
as simp rule explicitly if needed.

* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.

* Reorganized classes and locales for boolean algebras.
INCOMPATIBILITY.

* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
INCOMPATIBILITY.

* Sledgehammer:
 - Removed legacy "lam_lifting" (synonym for "lifting") from option
   "lam_trans". Minor INCOMPATIBILITY.
 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
   Minor INCOMPATIBILITY.
 - Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten
   using combinators, but the combinators are kept opaque, i.e. without
   definitions.

* Metis:
 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.


*** ML ***

* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
operations to accumulate items from types and terms, using a fast
syntactic order. The original order of occurrences may be recovered as
well, e.g. via TFrees.list_set.

* Thm.instantiate, Thm.generalize and related operations require
scalable datastructures from structure TVars, Vars, Names etc.
INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
accumulation of items.

* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
corresponding ML values, notably as arguments for Thm.instantiate etc.

* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
corresponding functions for the object-logic of the ML compilation
context. This supersedes older mk_Trueprop / dest_Trueprop operations.

* ML antiquotations for type constructors and term constants:

    \<^Type>\<open>c\<close>
    \<^Type>\<open>c T \<dots>\<close>       \<comment> \<open>same with type arguments\<close>
    \<^Type>_fn\<open>c T \<dots>\<close>    \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
    \<^Const>\<open>c\<close>
    \<^Const>\<open>c T \<dots>\<close>      \<comment> \<open>same with type arguments\<close>
    \<^Const>\<open>c for t \<dots>\<close>  \<comment> \<open>same with term arguments\<close>
    \<^Const_>\<open>c \<dots>\<close>       \<comment> \<open>same for patterns: case, let, fn\<close>
    \<^Const>_fn\<open>c T \<dots>\<close>   \<comment> \<open>fn abstraction, failure via exception TERM\<close>

Examples in HOL:

  val natT = \<^Type>\<open>nat\<close>;
  fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>;
  val dest_funT = fn \<^Type>\<open>fun A B\<close> => (A, B);
  fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>;
  val dest_conj = fn \<^Const_>\<open>conj for A B\<close> => (A, B);
  fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
  val dest_eq = fn \<^Const_>\<open>HOL.eq T for t u\<close> => (T, (t, u));

* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
For example:

  - type 'a Symtab.table etc.: build
  - type 'a Names.table etc.: build
  - type 'a list: build and build_rev
  - type Buffer.T: build and build_content

For example, see src/Pure/PIDE/xml.ML:

  val content_of = Buffer.build_content o fold add_content;

* ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on
the given ML expression, in contrast to functions "try" and "can" that
modify application of a function.

* ML antiquotations for conditional ML text:

    \<^if_linux>\<open>...\<close>
    \<^if_macos>\<open>...\<close>
    \<^if_windows>\<open>...\<close>
    \<^if_unix>\<open>...\<close>

* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.

The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
provide similar functionality as before. Rare INCOMPATIBILITY due to
subtle semantic differences:

  - Processes invoked from Isabelle/ML actually run in the context of
    the Java VM of Isabelle/Scala. The settings environment and current
    working directory are usually the same on both sides, but there can be
    subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).

  - Output via stdout and stderr is line-oriented: Unix vs. Windows
    line-endings are normalized towards Unix; presence or absence of a
    final newline is irrelevant. The original lines are available as
    Process_Result.out_lines/err_lines; the concatenated versions
    Process_Result.out/err *omit* a trailing newline (using
    Library.trim_line, which was occasional seen in applications before,
    but is no longer necessary).

  - Output needs to be plain text encoded in UTF-8: Isabelle/Scala
    recodes it temporarily as UTF-16. This works for well-formed Unicode
    text, but not for arbitrary byte strings. In such cases, the bash
    script should write tempory files, managed by Isabelle/ML operations
    like Isabelle_System.with_tmp_file to create a file name and
    File.read to retrieve its content.

  - Just like any other Scala function invoked from ML,
    Isabelle_System.bash_process requires a proper PIDE session context.
    This could be a regular batch session (e.g. "isabelle build"), a
    PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
    "isabelle dump" or "isabelle server"). Note that old "isabelle
    console" or raw "isabelle process" don't have that.

New Process_Result.timing works as in Isabelle/Scala, based on direct
measurements of the bash_process wrapper in C: elapsed time is always
available, CPU time is only available on Linux and macOS, GC time is
unavailable.

* Likewise, the following Isabelle/ML system operations are run in the
context of Isabelle/Scala:

  - Isabelle_System.make_directory
  - Isabelle_System.copy_dir
  - Isabelle_System.copy_file
  - Isabelle_System.copy_base_file
  - Isabelle_System.rm_tree
  - Isabelle_System.download


*** System ***

* Each Isabelle component may specify a Scala/Java jar module
declaratively via etc/build.props (file names are relative to the
component directory). E.g. see $ISABELLE_HOME/etc/build.props with
further explanations in the "system" manual.

* Command-line tool "isabelle scala_build" allows to invoke the build
process of all Scala/Java modules explicitly. Normally this is done
implicitly on demand, e.g. for "isabelle scala" or "isabelle jedit".

* Command-line tool "isabelle scala_project" is has been improved in
various ways:
  - sources from all components with etc/build.props are included,
  - sources of for the jEdit text editor and the Isabelle/jEdit
    plugins (jedit_base and jedit_main) are included by default,
  - more sources may be given on the command-line,
  - options -f and -D make the tool more convenient.

* Isabelle/jEdit is now composed more conventionally from the original
jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle
plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main
isabelle.jedit module is now part of Isabelle/Scala (as one big
$ISABELLE_SCALA_JAR).

* ML profiling has been updated and reactivated, after some degration in
Isabelle2021:

  - "isabelle build -o threads=1 -o profiling=..." works properly
    within the PIDE session context;

  - "isabelle profiling_report" now uses the session build database
    (like "isabelle log");

  - output uses non-intrusive tracing messages, instead of warnings.

* System option "system_log" specifies an optional log file for internal
messages produced by Output.system_message in Isabelle/ML; the value
"true" refers to console progress of the build job. This works for
"isabelle build" or any derivative of it.

* System options of type string may be set to "true" using the short
notation of type bool. E.g. "isabelle build -o system_log".

* System option "document=true" is an alias for "document=pdf" and thus
can be used in the short form. E.g. "isabelle build -o document".

* Command-line tool "isabelle version" supports repository archives
(without full .hg directory). More options.

* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
Note that only Windows supports old 32 bit executables, via settings
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).



New in Isabelle2021 (February 2021)
-----------------------------------

*** General ***

* On macOS, the IsabelleXYZ.app directory layout now follows the other
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY,
use e.g. IsabelleXYZ.app/bin/isabelle instead of former
IsabelleXYZ.app/Isabelle/bin/isabelle or
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle.

* HTML presentation uses rich markup produced by Isabelle/PIDE,
resulting in more colors and links.

* HTML presentation includes auxiliary files (e.g. ML) for each theory.

* Proof method "subst" is confined to the original subgoal range: its
included distinct_subgoals_tac no longer affects unrelated subgoals.
Rare INCOMPATIBILITY.

* Theory_Data extend operation is obsolete and needs to be the identity
function; merge should be conservative and not reset to the empty value.
Subtle INCOMPATIBILITY and change of semantics (due to
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
the begin of a new theory can be achieved via Theory.at_begin.


*** Isabelle/jEdit Prover IDE ***

* Improved GUI look-and-feel: the portable and scalable "FlatLaf Light"
is used by default on all platforms (appearance similar to IntelliJ
IDEA).

* Improved markup for theory header imports: hyperlinks for theory files
work without formal checking of content.

* The prover process can download auxiliary files (e.g. 'ML_file') for
theories with remote URL. This requires the external "curl" program.

* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
of the formal entity at the caret position.

* The visual feedback on caret entity focus is normally restricted to
definitions within the visible text area. The keyboard modifier "CS"
overrides this: then all defining and referencing positions are shown.
See also option "jedit_focus_modifier".

* The jEdit status line includes widgets both for JVM and ML heap usage.
Ongoing ML ongoing garbage collection is shown as "ML cleanup".

* The Monitor dockable provides buttons to request a full garbage
collection and sharing of live data on the ML heap. It also includes
information about the Java Runtime system.

* PIDE support for session ROOTS: markup for directories.

* Update to jedit-5.6.0, the latest release. This version works properly
on macOS by default, without the special MacOSX plugin.

* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
for better approximate window size on macOS and Linux/X11.

* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode,
but non-native look-and-feel (FlatLaf).

* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
viewer, instead of re-using the jEdit text editor.

* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
.ftl.tex extension. The corresponding Naproche-SAD server process can be
disabled by setting the system option naproche_server=false and
restarting the Isabelle application.


*** Document preparation ***

* Keyword 'document_theories' within ROOT specifies theories from other
sessions that should be included in the generated document source
directory. This does not affect the generated session.tex: \input{...}
needs to be used separately.

* The standard LaTeX engine is now lualatex, according to settings
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
pdflatex, but text encoding needs to conform strictly to utf8. Rare
INCOMPATIBILITY.

* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
document output is always PDF.

* Antiquotation @{tool} refers to Isabelle command-line tools, with
completion and formal reference to the source (external script or
internal Scala function).

* Antiquotation @{bash_function} refers to GNU bash functions that are
checked within the Isabelle settings environment.

* Antiquotations @{scala}, @{scala_object}, @{scala_type},
@{scala_method} refer to checked Isabelle/Scala entities.


*** Pure ***

* Session Pure-Examples contains notable examples for Isabelle/Pure
(former entries of HOL-Isar_Examples).

* Named contexts (locale and class specifications, locale and class
context blocks) allow bundle mixins for the surface context. This allows
syntax notations to be organized within bundles conveniently. See theory
"HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
manual for syntax descriptions.

* Definitions in locales produce rule which can be added as congruence
rule to protect foundational terms during simplification.

* Consolidated terminology and function signatures for nested targets:

  - Local_Theory.begin_nested replaces Local_Theory.open_target

  - Local_Theory.end_nested replaces Local_Theory.close_target

  - Combination of Local_Theory.begin_nested and
    Local_Theory.end_nested(_result) replaces
    Local_Theory.subtarget(_result)

INCOMPATIBILITY.

* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.


*** HOL ***

* Session HOL-Examples contains notable examples for Isabelle/HOL
(former entries of HOL-Isar_Examples, HOL-ex etc.).

* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.

* Zipperposition 2.0 is now included as Isabelle component for
experimentation, e.g. in "sledgehammer [prover = zipperposition]".

* Sledgehammer:
  - support veriT in proof preplay
  - take adventage of more cores in proof preplay

* Updated the Metis prover underlying the "metis" proof method to
version 2.4 (release 20180810). The new version fixes one soundness
defect and two incompleteness defects. Very slight INCOMPATIBILITY.

* Nitpick/Kodkod may be invoked directly within the running
Isabelle/Scala session (instead of an external Java process): this
improves reactivity and saves resources. This experimental feature is
guarded by system option "kodkod_scala" (default: true in PIDE
interaction, false in batch builds).

* Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
INCOMPATIBILITY, consider repairing proofs locally like this:

  supply subst_all [simp del] [[simproc del: defined_all]]

* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
on datatypes to "False" if either side is a proper subexpression of the
other (for any datatype with a reasonable size function).

* Syntax for state monad combinators fcomp and scomp is organized in
bundle state_combinator_syntax.  Minor INCOMPATIBILITY.

* Syntax for reflected term syntax is organized in bundle term_syntax,
discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.

* New constant "power_int" for exponentiation with integer exponent,
written as "x powi n".

* Added the "at most 1" quantifier, Uniq.

* For the natural numbers, "Sup {} = 0".

* New constant semiring_char gives the characteristic of any type of
class semiring_1, with the convenient notation CHAR('a). For example,
CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17.

* HOL-Computational_Algebra.Polynomial: Definition and basic properties
of algebraic integers.

* Library theory "Bit_Operations" with generic bit operations.

* Library theory "Signed_Division" provides operations for signed
division, instantiated for type int.

* Theory "Multiset": removed misleading notation \<Union># for sum_mset;
replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now.

* New theory "HOL-Library.Word" takes over material from former session
"HOL-Word". INCOMPATIBILITY: need to adjust imports.

* Theory "HOL-Library.Word": Type word is restricted to bit strings
consisting of at least one bit. INCOMPATIBILITY.

* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based
on generic algebraic bit operations from theory
"HOL-Library.Bit_Operations". INCOMPATIBILITY.

* Theory "HOL-Library.Word": Most operations on type word are set up for
transfer and lifting. INCOMPATIBILITY.

* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY,
sometimes additional rewrite rules must be added to applications to get
a confluent system again.

* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for
both types int and word. INCOMPATIBILITY.

* Theory "HOL-Library.Word": Syntax for signed compare operators has
been consolidated with syntax of regular compare operators. Minor
INCOMPATIBILITY.

* Former session "HOL-Word": Various operations dealing with bit values
represented as reversed lists of bools are separated into theory
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.

* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.

* Former session "HOL-Word": Compound operation "bin_split" simplifies
by default into its components "drop_bit" and "take_bit".
INCOMPATIBILITY.

* Former session "HOL-Word": Operations lsb, msb and set_bit are
separated into theories Least_significant_bit, Most_significant_bit and
Generic_set_bit respectively in session Word_Lib in the AFP.
INCOMPATIBILITY.

* Former session "HOL-Word": Ancient int numeral representation has been
factored out in separate theory "Ancient_Numeral" in session Word_Lib in
the AFP. INCOMPATIBILITY.

* Former session "HOL-Word": Operations "bin_last", "bin_rest",
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.

* Former session "HOL-Word": Misc ancient material has been factored out
into separate theories and moved to session Word_Lib in the AFP. See
theory "Guide" there for further information. INCOMPATIBILITY.

* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
are in working order again, as opposed to outputting "GaveUp" on nearly
all problems.

* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
abstract language constructors.

* Session "HOL-Hoare": now provides a total correctness logic as well.


*** FOL ***

* Added the "at most 1" quantifier, Uniq, as in HOL.

* Simproc "defined_all" and rewrite rule "subst_all" have been changed
as in HOL.


*** ML ***

* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
registered Isabelle/Scala functions (of type String => String):
invocation works via the PIDE protocol.

* Path.append is available as overloaded "+" operator, similar to
corresponding Isabelle/Scala operation.

* ML statistics via an external Poly/ML process: this allows monitoring
the runtime system while the ML program sleeps.


*** System ***

* Isabelle server allows user-defined commands via
isabelle_scala_service.

* Update/rebuild external provers on currently supported OS platforms,
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.

* The command-line tool "isabelle log" prints prover messages from the
build database of the given session, following the the order of theory
sources, instead of erratic parallel evaluation. Consequently, the
session log file is restricted to system messages of the overall build
process, and thus becomes more informative.

* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.

* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
(for DVI documents) has been discontinued. Former option -n has been
turned into -o with explicit file name. Minor INCOMPATIBILITY.

* The command-line tool "isabelle components" supports new options -u
and -x to manage $ISABELLE_HOME_USER/etc/components without manual
editing of Isabelle configuration files.

* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
session databases. It used to be hard-wired for Isabelle + AFP, but
other projects may now participate on equal terms.

* The command-line tool "isabelle process" now prints output to
stdout/stderr separately and incrementally, instead of just one bulk to
stdout after termination. Potential INCOMPATIBILITY for external tools.

* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).

* Batch-builds via "isabelle build" use a PIDE session with special
protocol: this allows to invoke Isabelle/Scala operations from
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:

  ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"

This includes full PIDE markup, if option "build_pide_reports" is
enabled.

* The command-line tool "isabelle build" provides option -P DIR to
produce PDF/HTML presentation in the specified directory; -P: refers to
the standard directory according to ISABELLE_BROWSER_INFO /
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
from the build database -- from this or earlier builds with option
document=pdf.

* The command-line tool "isabelle document" generates theory documents
on the spot, using the underlying session build database (exported
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
"isabelle document" tool was rather different and has been discontinued.

* The command-line tool "isabelle sessions" explores the structure of
Isabelle sessions and prints result names in topological order (on
stdout).

* The Isabelle/Scala "Progress" interface changed slightly and
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
instead.

* General support for Isabelle/Scala system services, configured via the
shell function "isabelle_scala_service" in etc/settings (e.g. of an
Isabelle component); see implementations of class
Isabelle_System.Service in Isabelle/Scala. This supersedes former
"isabelle_scala_tools" and "isabelle_file_format": minor
INCOMPATIBILITY.

* The syntax of theory load commands (for auxiliary files) is now
specified in Isabelle/Scala, as instance of class
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
in etc/settings. This allows more flexible schemes than just a list of
file extensions. Minor INCOMPATIBILITY, e.g. see theory
HOL-SPARK.SPARK_Setup to emulate the old behaviour.

* JVM system property "isabelle.laf" has been discontinued; the default
Swing look-and-feel is ""FlatLaf Light".

* Isabelle/Phabricator supports Ubuntu 20.04 LTS.

* Isabelle/Phabricator setup has been updated to follow ongoing
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
existing server installations should remove libphutil from
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
directory (e.g. /var/www/phabricator-vcs/libphutil).

* Experimental support for arm64-linux platform. The reference platform
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).

* Support for Apple Silicon, using mostly x86_64-darwin runtime
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
some native arm64-darwin executables (e.g. Java).



New in Isabelle2020 (April 2020)
--------------------------------

*** General ***

* Session ROOT files need to specify explicit 'directories' for import
of theory files. Directories cannot be shared by different sessions.
(Recall that import of theories from other sessions works via
session-qualified theory names, together with suitable 'sessions'
declarations in the ROOT.)

* Internal derivations record dependencies on oracles and other theorems
accurately, including the implicit type-class reasoning wrt. proven
class relations and type arities. In particular, the formal tagging with
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
propagated properly to theorems depending on such type instances.

* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
actual proposition that is assumed in the goal and proof context. This
requires at least Proofterm.proofs = 1 to show up in theorem
dependencies.

* Command 'thm_oracles' prints all oracles used in given theorems,
covering the full graph of transitive dependencies.

* Command 'thm_deps' prints immediate theorem dependencies of the given
facts. The former graph visualization has been discontinued, because it
was hardly usable.

* Refined treatment of proof terms, including type-class proofs for
minor object-logics (FOL, FOLP, Sequents).

* The inference kernel is now confined to one main module: structure
Thm, without the former circular dependency on structure Axclass.

* Mixfix annotations may use "' " (single quote followed by space) to
separate delimiters (as documented in the isar-ref manual), without
requiring an auxiliary empty block. A literal single quote needs to be
escaped properly. Minor INCOMPATIBILITY.


*** Isar ***

* The proof method combinator (subproofs m) applies the method
expression m consecutively to each subgoal, constructing individual
subproofs internally. This impacts the internal construction of proof
terms: it makes a cascade of let-expressions within the derivation tree
and may thus improve scalability.

* Attribute "trace_locales" activates tracing of locale instances during
roundup. It replaces the diagnostic command 'print_dependencies', which
has been discontinued.


*** Isabelle/jEdit Prover IDE ***

* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
the "session focus" of option "isabelle jedit -S" has become obsolete
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
sufficient and more convenient to start editing a particular session.

* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
tooltip message popups, corresponding to mouse hovering with/without the
CONTROL/COMMAND key pressed.

* The following actions allow to navigate errors within the current
document snapshot:

  isabelle.first-error (CS+a)
  isabelle.last-error (CS+z)
  isabelle.next-error (CS+n)
  isabelle.prev-error (CS+p)

* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).

* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
Monitor) applies the jconsole tool on the running Isabelle/jEdit
process. This allows to monitor resource usage etc.

* More adequate default font sizes for Linux on HD / UHD displays:
automatic font scaling is usually absent on Linux, in contrast to
Windows and macOS.

* The default value for the jEdit property "view.antiAlias" (menu item
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
now "subpixel HRGB", instead of former "standard". Especially on Linux
this often leads to faster text rendering, but can also cause problems
with odd color shades. An alternative is to switch back to "standard"
here, and set the following Java system property:

    isabelle jedit -Dsun.java2d.opengl=true

This can be made persistent via JEDIT_JAVA_OPTIONS in
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
application there is a corresponding options file in the same directory.


*** Isabelle/VSCode Prover IDE ***

* Update of State and Preview panels to use new WebviewPanel API of
VSCode.


*** HOL ***

* Improvements of the 'lift_bnf' command:
  - Add support for quotient types.
  - Generate transfer rules for the lifted map/set/rel/pred constants
    (theorems "<type>.<constant>_transfer_raw").

* Term_XML.Encode/Decode.term uses compact representation of Const
"typargs" from the given declaration environment. This also makes more
sense for translations to lambda-calculi with explicit polymorphism.
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
applications.

* ASCII membership syntax concerning big operators for infimum and
supremum has been discontinued. INCOMPATIBILITY.

* Removed multiplicativity assumption from class
"normalization_semidom". Introduced various new intermediate classes
with the multiplicativity assumption; many theorem statements
(especially involving GCD/LCM) had to be adapted. This allows for a more
natural instantiation of the algebraic typeclasses for e.g. Gaussian
integers. INCOMPATIBILITY.

* Clear distinction between types for bits (False / True) and Z2 (0 /
1): theory HOL-Library.Bit has been renamed accordingly.
INCOMPATIBILITY.

* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
to algebra_simps and field_simps but contain more aggressive rules
potentially splitting goals; algebra_split_simps roughly replaces
sign_simps and field_split_simps can be used instead of divide_simps.
INCOMPATIBILITY.

* Theory HOL.Complete_Lattices:
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf

* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
associates to the left now as is customary.

* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
multiple colours and arbitrary exponents.

* Session HOL-Proofs: build faster thanks to better treatment of proof
terms in Isabelle/Pure.

* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
INCOMPATIBILITY.

* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.

* Session HOL-Complex_Analysis has been split off from HOL-Analysis.


*** ML ***

* Theory construction may be forked internally, the operation
Theory.join_theory recovers a single result theory. See also the example
in theory "HOL-ex.Join_Theory".

* Antiquotation @{oracle_name} inlines a formally checked oracle name.

* Minimal support for a soft-type system within the Isabelle logical
framework (module Soft_Type_System).

* Former Variable.auto_fixes has been replaced by slightly more general
Proof_Context.augment: it is subject to an optional soft-type system of
the underlying object-logic. Minor INCOMPATIBILITY.

* More scalable Export.export using XML.tree to avoid premature string
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.

* Prover IDE support for the underlying Poly/ML compiler (not the basis
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
implementation with full markup.


*** System ***

* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>

* The command-line tool "isabelle scala_project" creates a Gradle
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
such as IntelliJ IDEA.

* The command-line tool "isabelle phabricator_setup" facilitates
self-hosting of the Phabricator software-development platform, with
support for Git, Mercurial, Subversion repositories. This helps to avoid
monoculture and to escape the gravity of centralized version control by
Github and/or Bitbucket. For further documentation, see chapter
"Phabricator server administration" in the "system" manual. A notable
example installation is https://isabelle-dev.sketis.net/.

* The command-line tool "isabelle hg_setup" simplifies the setup of
Mercurial repositories, with hosting via Phabricator or SSH file server
access.

* The command-line tool "isabelle imports" has been discontinued: strict
checking of session directories enforces session-qualified theory names
in applications -- users are responsible to specify session ROOT entries
properly.

* The command-line tool "isabelle dump" and its underlying
Isabelle/Scala module isabelle.Dump has become more scalable, by
splitting sessions and supporting a base logic image. Minor
INCOMPATIBILITY in options and parameters.

* The command-line tool "isabelle build_docker" has been slightly
improved: it is now properly documented in the "system" manual.

* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
users, system services.

* Isabelle/Scala support for proof terms (with full type/term
information) in module isabelle.Term.

* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
"isabelle dump".

* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
exported as well: this spans an overall dependency graph of internal
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.

* Theory export of structured specifications, based on internal
declarations of Spec_Rules by packages like 'definition', 'inductive',
'primrec', 'function'.

* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.

* More complete x86_64 platform support on macOS, notably Catalina where
old x86 has been discontinued.

* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.

* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).



New in Isabelle2019 (June 2019)
-------------------------------

*** General ***

* The font collection "Isabelle DejaVu" is systematically derived from
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
"IsabelleText" font (which is no longer provided separately). The line
metrics and overall rendering quality is closer to original DejaVu.
INCOMPATIBILITY with display configuration expecting the old
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.

* The Isabelle fonts render "\<inverse>" properly as superscript "-1".

* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).

* Old-style {* verbatim *} tokens are explicitly marked as legacy
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
via "isabelle update_cartouches -t" (available since Isabelle2015).

* Infix operators that begin or end with a "*" are now parenthesized
without additional spaces, e.g. "(*)" instead of "( * )". Minor
INCOMPATIBILITY.

* Mixfix annotations may use cartouches instead of old-style double
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
mixfix_cartouches" allows to update existing theory sources
automatically.

* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
need to provide a closed expression -- without trailing semicolon. Minor
INCOMPATIBILITY.

* Commands 'generate_file', 'export_generated_files', and
'compile_generated_files' support a stateless (PIDE-conformant) model
for generated sources and compiled binaries of other languages. The
compilation process is managed in Isabelle/ML, and results exported to
the session database for further use (e.g. with "isabelle export" or
"isabelle build -e").


*** Isabelle/jEdit Prover IDE ***

* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. Line spacing no longer needs to be
adjusted: properties for the old IsabelleText font had "Global Options /
Text Area / Extra vertical line spacing (in pixels): -2", it now
defaults to 1, but 0 works as well.

* The jEdit File Browser is more prominent in the default GUI layout of
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
resources, notably via "favorites:" (or "Edit Favorites").

* Further markup and rendering for "plain text" (e.g. informal prose)
and "raw text" (e.g. verbatim sources). This improves the visual
appearance of formal comments inside the term language, or in general
for repeated alternation of formal and informal text.

* Action "isabelle-export-browser" points the File Browser to the theory
exports of the current buffer, based on the "isabelle-export:" virtual
file-system. The directory view needs to be reloaded manually to follow
ongoing document processing.

* Action "isabelle-session-browser" points the File Browser to session
information, based on the "isabelle-session:" virtual file-system. Its
entries are structured according to chapter / session names, the open
operation is redirected to the session ROOT file.

* Support for user-defined file-formats via class isabelle.File_Format
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
the shell function "isabelle_file_format" in etc/settings (e.g. of an
Isabelle component).

* System option "jedit_text_overview" allows to disable the text
overview column.

* Command-line options "-s" and "-u" of "isabelle jedit" override the
default for system option "system_heaps" that determines the heap
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".

* The Isabelle/jEdit desktop application uses the same options as
"isabelle jedit" for its internal "isabelle build" process: the implicit
option "-o system_heaps" (or "-s") has been discontinued. This reduces
the potential for surprise wrt. command-line tools.

* The official download of the Isabelle/jEdit application already
contains heap images for Isabelle/HOL within its main directory: thus
the first encounter becomes faster and more robust (e.g. when run from a
read-only directory).

* Isabelle DejaVu fonts are available with hinting by default, which is
relevant for low-resolution displays. This may be disabled via system
option "isabelle_fonts_hinted = false" in
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
results.

* OpenJDK 11 has quite different font rendering, with better glyph
shapes and improved sub-pixel anti-aliasing. In some situations results
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
display is recommended.

* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
property jdk.gtk.version). The factory default is version 3, but
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
this more conservative (as in Java 8). Depending on the GTK theme
configuration, "-Djdk.gtk.version=3" might work better or worse.


*** Document preparation ***

* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
are stripped from document output: the effect is to modify the semantic
presentation context or to emit markup to the PIDE document. Some
predefined markers are taken from the Dublin Core Metadata Initiative,
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
can be retrieved from the document database.

* Old-style command tags %name are re-interpreted as markers with
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
before. Potential INCOMPATIBILITY: multiple markers are composed in
canonical order, resulting in a reversed list of tags in the
presentation context.

* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
of semantics wrt. old-style %name.

* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
template.

* Document antiquotation option "cartouche" indicates if the output
should be delimited as cartouche; this takes precedence over the
analogous option "quotes".

* Many document antiquotations are internally categorized as "embedded"
and expect one cartouche argument, which is typically used with the
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
delimiters are stripped in output of the source (antiquotation option
"source"), but it is possible to enforce delimiters via option
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.


*** Isar ***

* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).

* More robust treatment of structural errors: begin/end blocks take
precedence over goal/proof. This is particularly relevant for the
headless PIDE session and server.

* Command keywords of kind thy_decl / thy_goal may be more specifically
fit into the traditional document model of "definition-statement-proof"
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.


*** HOL ***

* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.

* Command 'export_code': the 'file' argument is now legacy and will be
removed soon: writing to the physical file-system is not well-defined in
a reactive/parallel application like Isabelle. The empty 'file' argument
has been discontinued already: it is superseded by the file-browser in
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.

* Command 'code_reflect' no longer supports the 'file' argument: it has
been superseded by 'file_prefix' for stateless file management as in
'export_code'. Minor INCOMPATIBILITY.

* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.

* Code generation for OCaml: Zarith supersedes Nums as library for
proper integer arithmetic. The library is located via standard
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
The environment provided by "isabelle ocaml_setup" already contains this
tool and the required packages. Minor INCOMPATIBILITY.

* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
INCOMPATIBILITY.

* Code generation: slightly more conventional syntax for 'code_stmts'
antiquotation. Minor INCOMPATIBILITY.

* Theory List: the precedence of the list_update operator has changed:
"f a [n := x]" now needs to be written "(f a)[n := x]".

* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
now have the same precedence as any other prefix function symbol. Minor
INCOMPATIBILITY.

* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
SUPREMUM, UNION, INTER should now rarely occur in output and are just
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
are gone INCOMPATIBILITY.

* The simplifier uses image_cong_simp as a congruence rule. The historic
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
not used by default any longer. INCOMPATIBILITY; consider using declare
image_cong_simp [cong del] in extreme situations.

* INF_image and SUP_image are no default simp rules any longer.
INCOMPATIBILITY, prefer image_comp as simp rule if needed.

* Strong congruence rules (with =simp=> in the premises) for constant f
are now uniformly called f_cong_simp, in accordance with congruence
rules produced for mappers by the datatype package. INCOMPATIBILITY.

* Retired lemma card_Union_image; use the simpler card_UN_disjoint
instead. INCOMPATIBILITY.

* Facts sum_mset.commute and prod_mset.commute have been renamed to
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.

* ML structure Inductive: slightly more conventional naming schema.
Minor INCOMPATIBILITY.

* ML: Various _global variants of specification tools have been removed.
Minor INCOMPATIBILITY, prefer combinators
Named_Target.theory_map[_result] to lift specifications to the global
theory level.

* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
overlapping and non-exhaustive patterns and handles arbitrarily nested
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
assumes sequential left-to-right pattern matching. The generated
equation no longer tuples the arguments on the right-hand side.
INCOMPATIBILITY.

* Theory HOL-Library.Multiset: the \<Union># operator now has the same
precedence as any other prefix function symbol.

* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
of the bundle cardinal_syntax (available in theory Main). Minor
INCOMPATIBILITY.

* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
used for computing powers in class "monoid_mult" and modular
exponentiation.

* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
of Formal power series.

* Session HOL-Number_Theory: More material on residue rings in
Carmichael's function, primitive roots, more properties for "ord".

* Session HOL-Analysis: Better organization and much more material
at the level of abstract topological spaces.

* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
 algebraic closure of a field by de Vilhena and Baillon.

* Session HOL-Homology has been added. It is a port of HOL Light's
homology library, with new proofs of "invariance of domain" and related
results.

* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
command-line.

* Sledgehammer:
  - The URL for SystemOnTPTP, which is used by remote provers, has been
    updated.
  - The machine-learning-based filter MaSh has been optimized to take
    less time (in most cases).

* SMT: reconstruction is now possible using the SMT solver veriT.

* Session HOL-Word:
  * New theory More_Word as comprehensive entrance point.
  * Merged type class bitss into type class bits.
  INCOMPATIBILITY.


*** ML ***

* Command 'generate_file' allows to produce sources for other languages,
with antiquotations in the Isabelle context (only the control-cartouche
form). The default "cartouche" antiquotation evaluates an ML expression
of type string and inlines the result as a string literal of the target
language. For example, this works for Haskell as follows:

  generate_file "Pure.hs" = \<open>
  module Isabelle.Pure where
    allConst, impConst, eqConst :: String
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
  \<close>

See also commands 'export_generated_files' and 'compile_generated_files'
to use the results.

* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML.

* ML antiquotation @{master_dir} refers to the master directory of the
underlying theory, i.e. the directory of the theory file.

* ML antiquotation @{verbatim} inlines its argument as string literal,
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
useful.

* Local_Theory.reset is no longer available in user space. Regular
definitional packages should use balanced blocks of
Local_Theory.open_target versus Local_Theory.close_target instead, or
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.

* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").


*** System ***

* Update to OpenJDK 11: the current long-term support version of Java.

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.

* System option "checkpoint" has been discontinued: obsolete thanks to
improved memory management in Poly/ML.

* System option "system_heaps" determines where to store the session