NEWS

avoid fact name clashes

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 ***

* 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).

* 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.

* Session ROOT entries no longer allow specification of 'files'. Rare
INCOMPATIBILITY, use command 'external_file' within a proper theory
context.

* Session root directories may be specified multiple times: each
accessible ROOT file is processed only once. This facilitates
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
-d or -D for "isabelle build" and "isabelle jedit". Example:

  isabelle build -D '~~/src/ZF'


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Completion supports theory header imports.


*** HOL ***

* 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.

* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.


*** System ***

* Windows and Cygwin is for x86_64 only. Old 32bit platform support has
been discontinued.

* Command-line tool "isabelle build" supports new options:
  - option -B NAME: include session NAME and all descendants
  - option -S: only observe changes of sources, not heap images


New in Isabelle2017 (October 2017)
----------------------------------

*** General ***

* Experimental support for Visual Studio Code (VSCode) as alternative
Isabelle/PIDE front-end, see also
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017

VSCode is a new type of application that continues the concepts of
"programmer's editor" and "integrated development environment" towards
fully semantic editing and debugging -- in a relatively light-weight
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
Technically, VSCode is based on the Electron application framework
(Node.js + Chromium browser + V8), which is implemented in JavaScript
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
modules around a Language Server implementation.

* Theory names are qualified by the session name that they belong to.
This affects imports, but not the theory name space prefix (which is
just the theory base name as before).

In order to import theories from other sessions, the ROOT file format
provides a new 'sessions' keyword. In contrast, a theory that is
imported in the old-fashioned manner via an explicit file-system path
belongs to the current session, and might cause theory name conflicts
later on. Theories that are imported from other sessions are excluded
from the current session document. The command-line tool "isabelle
imports" helps to update theory imports.

* The main theory entry points for some non-HOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:

  CTT/Main.thy    ~>  CTT/CTT.thy
  ZF/Main.thy     ~>  ZF/ZF.thy
  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
  ZF/ZF.thy       ~>  ZF/ZF_Base.thy

INCOMPATIBILITY.

* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to name-space
accesses within global or local theory contexts, e.g. within a 'bundle'.

* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.

* Computations generated by the code generator can be embedded directly
into ML, alongside with @{code} antiquotations, using the following
antiquotations:

  @{computation ... terms: ... datatypes: ...} :
    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
  @{computation_conv ... terms: ... datatypes: ...} :
    (Proof.context -> 'ml -> conv) -> Proof.context -> conv
  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv

See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Session-qualified theory imports allow the Prover IDE to process
arbitrary theory hierarchies independently of the underlying logic
session image (e.g. option "isabelle jedit -l"), but the directory
structure needs to be known in advance (e.g. option "isabelle jedit -d"
or a line in the file $ISABELLE_HOME_USER/ROOTS).

* The PIDE document model maintains file content independently of the
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
changes of formal document content. Theory dependencies are always
resolved internally, without the need for corresponding editor buffers.
The system option "jedit_auto_load" has been discontinued: it is
effectively always enabled.

* The Theories dockable provides a "Purge" button, in order to restrict
the document model to theories that are required for open editor
buffers.

* The Theories dockable indicates the overall status of checking of each
entry. When all forked tasks of a theory are finished, the border is
painted with thick lines; remaining errors in this situation are
represented by a different border color.

* Automatic indentation is more careful to avoid redundant spaces in
intermediate situations. Keywords are indented after input (via typed
characters or completion); see also option "jedit_indent_input".

* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.

* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
entry of the specified logic session in the editor, while its parent is
used for formal checking.

* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
enabled at all times.

* Update to current jedit-5.4.0.


*** Pure ***

* Deleting the last code equations for a particular function using
[code del] results in function with no equations (runtime abort) rather
than an unimplemented function (generation time abort). Use explicit
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.

* Proper concept of code declarations in code.ML:
  - Regular code declarations act only on the global theory level, being
    ignored with warnings if syntactically malformed.
  - Explicitly global code declarations yield errors if syntactically
    malformed.
  - Default code declarations are silently ignored if syntactically
    malformed.
Minor INCOMPATIBILITY.

* Clarified and standardized internal data bookkeeping of code
declarations: history of serials allows to track potentially
non-monotonous declarations appropriately. Minor INCOMPATIBILITY.


*** HOL ***

* The Nunchaku model finder is now part of "Main".

* SMT module:
  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
    'int' and benefit from the SMT solver's theory reasoning. It is
    disabled by default.
  - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
  - Several small issues have been rectified in the 'smt' command.

* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
generated for datatypes with type class annotations. As a result, the
tactic that derives it no longer fails on nested datatypes. Slight
INCOMPATIBILITY.

* Command and antiquotation "value" with modified default strategy:
terms without free variables are always evaluated using plain evaluation
only, with no fallback on normalization by evaluation. Minor
INCOMPATIBILITY.

* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").

* Constant "surj" is a full input/output abbreviation (again).
Minor INCOMPATIBILITY.

* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.

* Renamed ii to imaginary_unit in order to free up ii as a variable
name. The syntax \<i> remains available. INCOMPATIBILITY.

* Dropped abbreviations transP, antisymP, single_valuedP; use constants
transp, antisymp, single_valuedp instead. INCOMPATIBILITY.

* Constant "subseq" in Topological_Spaces has been removed -- it is
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.

* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.

* Theory List: new generic function "sorted_wrt".

* Named theorems mod_simps covers various congruence rules concerning
mod, replacing former zmod_simps. INCOMPATIBILITY.

* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
mod_diff_eq. INCOMPATIBILITY.

* Generalized some facts:
    measure_induct_rule
    measure_induct
    zminus_zmod ~> mod_minus_eq
    zdiff_zmod_left ~> mod_diff_left_eq
    zdiff_zmod_right ~> mod_diff_right_eq
    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
INCOMPATIBILITY.

* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
unique_euclidean_(semi)ring; instantiation requires provision of a
euclidean size.

* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
  - Euclidean induction is available as rule eucl_induct.
  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
  - Coefficients obtained by extended euclidean algorithm are
    available as "bezout_coefficients".
INCOMPATIBILITY.

* Theory "Number_Theory.Totient" introduces basic notions about Euler's
totient function previously hidden as solitary example in theory
Residues. Definition changed so that "totient 1 = 1" in agreement with
the literature. Minor INCOMPATIBILITY.

* New styles in theory "HOL-Library.LaTeXsugar":
  - "dummy_pats" for printing equations with "_" on the lhs;
  - "eta_expand" for printing eta-expanded terms.

* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.

* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
filter for describing points x such that f(x) is in the filter F.

* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
space. INCOMPATIBILITY.

* Theory "HOL-Library.FinFun" has been moved to AFP (again).
INCOMPATIBILITY.

* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
replacement syntax has been removed. INCOMPATIBILITY, standard syntax
with symbols should be used instead. The subsequent commands help to
reproduce the old forms, e.g. to simplify porting old theories:

syntax (ASCII)
  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)

* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
multisets have been renamed:

  msetless_cancel_numerals ~> msetsubset_cancel
  msetle_cancel_numerals ~> msetsubset_eq_cancel

INCOMPATIBILITY.

* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.

* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.

* Session HOL-Analysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts, infinite products, simplicial
complexes. Baire Category theorem. Major results include the Jordan
Curve Theorem and the Great Picard Theorem.

* Session HOL-Algebra has been extended by additional lattice theory:
the Knaster-Tarski fixed point theorem and Galois Connections.

* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
of squarefreeness, n-th powers, and prime powers.

* Session "HOL-Computional_Algebra" covers many previously scattered
theories, notably Euclidean_Algorithm, Factorial_Ring,
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
INCOMPATIBILITY.


*** System ***

* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or full-scale server
(PostgreSQL via local port or remote ssh connection).

* Results of "isabelle build" are recorded as SQLite database (i.e.
"Application File Format" in the sense of
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.

* System option "parallel_proofs" is 1 by default (instead of more
aggressive 2). This requires less heap space and avoids burning parallel
CPU cycles, while full subproof parallelization is enabled for repeated
builds (according to parallel_subproofs_threshold).

* System option "record_proofs" allows to change the global
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
a negative value means the current state in the ML heap image remains
unchanged.

* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.

* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
native Windows platform (independently of the Cygwin installation). This
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
ISABELLE_PLATFORM64.

* Command-line tool "isabelle build_docker" builds a Docker image from
the Isabelle application bundle for Linux. See also
https://hub.docker.com/r/makarius/isabelle

* Command-line tool "isabelle vscode_server" provides a Language Server
Protocol implementation, e.g. for the Visual Studio Code editor. It
serves as example for alternative PIDE front-ends.

* Command-line tool "isabelle imports" helps to maintain theory imports
wrt. session structure. Examples for the main Isabelle distribution:

  isabelle imports -I -a
  isabelle imports -U -a
  isabelle imports -U -i -a
  isabelle imports -M -a -d '~~/src/Benchmarks'


New in Isabelle2016-1 (December 2016)
-------------------------------------

*** General ***

* Splitter in proof methods "simp", "auto" and friends:
  - The syntax "split add" has been discontinued, use plain "split",
    INCOMPATIBILITY.
  - For situations with many conditional or case expressions, there is
    an alternative splitting strategy that can be much faster. It is
    selected by writing "split!" instead of "split". It applies safe
    introduction and elimination rules after each split rule. As a
    result the subgoal may be split into several subgoals.

* Command 'bundle' provides a local theory target to define a bundle
from the body of specification commands (such as 'declare',
'declaration', 'notation', 'lemmas', 'lemma'). For example:

bundle foo
begin
  declare a [simp]
  declare b [intro]
end

* Command 'unbundle' is like 'include', but works within a local theory
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.

* Simplified outer syntax: uniform category "name" includes long
identifiers. Former "xname" / "nameref" / "name reference" has been
discontinued.

* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.

* Mixfix annotations support general block properties, with syntax
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.

* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.

* Commands 'prf' and 'full_prf' are somewhat more informative (again):
proof terms are reconstructed and cleaned from administrative thm nodes.

* Code generator: config option "code_timing" triggers measurements of
different phases of code generation. See src/HOL/ex/Code_Timing.thy for
examples.

* Code generator: implicits in Scala (stemming from type class
instances) are generated into companion object of corresponding type
class, to resolve some situations where ambiguities may occur.

* Solve direct: option "solve_direct_strict_warnings" gives explicit
warnings for lemma statements with trivial proofs.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* More aggressive flushing of machine-generated input, according to
system option editor_generated_input_delay (in addition to existing
editor_input_delay for regular user edits). This may affect overall PIDE
reactivity and CPU usage.

* Syntactic indentation according to Isabelle outer syntax. Action
"indent-lines" (shortcut C+i) indents the current line according to
command keywords and some command substructure. Action
"isabelle.newline" (shortcut ENTER) indents the old and the new line
according to command keywords only; see also option
"jedit_indent_newline".

* Semantic indentation for unstructured proof scripts ('apply' etc.) via
number of subgoals. This requires information of ongoing document
processing and may thus lag behind, when the user is editing too
quickly; see also option "jedit_script_indent" and
"jedit_script_indent_limit".

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure; 'begin' and 'end'
structure of theory specifications is treated as well.

* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".

* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.

* Sidekick parser "isabelle-context" shows nesting of context blocks
according to 'begin' and 'end' structure.

* Highlighting of entity def/ref positions wrt. cursor.

* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurrences of the formal entity at the caret position. This facilitates
systematic renaming.

* PIDE document markup works across multiple Isar commands, e.g. the
results established at the end of a proof are properly identified in the
theorem statement.

* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.

* Dockable window "Symbols" also provides access to 'abbrevs' from the
outer syntax of the current theory buffer. This provides clickable
syntax templates, including entries with empty abbrevs name (which are
inaccessible via keyboard completion).

* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:

  src/Pure/ROOT0.ML
  src/Pure/ROOT.ML
  src/Pure/Pure.thy
  src/Pure/ML_Bootstrap.thy

The ML ROOT files act like quasi-theories in the context of theory
ML_Bootstrap: this allows continuous checking of all loaded ML files.
The theory files are presented with a modified header to import Pure
from the running Isabelle instance. Results from changed versions of
each stage are *not* propagated to the next stage, and isolated from the
actual Isabelle/Pure that runs the IDE itself. The sequential
dependencies of the above files are only observed for batch build.

* Isabelle/ML and Standard ML files are presented in Sidekick with the
tree structure of section headings: this special comment format is
described in "implementation" chapter 0, e.g. (*** section ***).

* Additional abbreviations for syntactic completion may be specified
within the theory header as 'abbrevs'. The theory syntax for 'keywords'
has been simplified accordingly: optional abbrevs need to go into the
new 'abbrevs' section.

* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
INCOMPATIBILITY, use 'abbrevs' within theory header instead.

* Action "isabelle.keymap-merge" asks the user to resolve pending
Isabelle keymap changes that are in conflict with the current jEdit
keymap; non-conflicting changes are always applied implicitly. This
action is automatically invoked on Isabelle/jEdit startup and thus
increases chances that users see new keyboard shortcuts when re-using
old keymaps.

* ML and document antiquotations for file-systems paths are more uniform
and diverse:

  @{path NAME}   -- no file-system check
  @{file NAME}   -- check for plain file
  @{dir NAME}    -- check for directory

Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
have to be changed.


*** Document preparation ***

* New symbol \<circle>, e.g. for temporal operator.

* New document and ML antiquotation @{locale} for locales, similar to
existing antiquotation @{class}.

* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
this allows special forms of document output.

* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
derivatives.

* \<^raw:...> symbols are no longer supported.

* Old 'header' command is no longer supported (legacy since
Isabelle2015).


*** Isar ***

* Many specification elements support structured statements with 'if' /
'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
'definition', 'inductive', 'function'.

* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the
context: INCOMPATIBILITY.

* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
'definition' and 'obtain'. It fits better into the Isar language than
old 'def', which is now a legacy feature.

* Command 'obtain' supports structured statements with 'if' / 'for'
context.

* Command '\<proof>' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.

* The defining position of a literal fact \<open>prop\<close> is maintained more
carefully, and made accessible as hyperlink in the Prover IDE.

* Commands 'finally' and 'ultimately' used to expose the result as
literal fact: this accidental behaviour has been discontinued. Rare
INCOMPATIBILITY, use more explicit means to refer to facts in Isar.

* Command 'axiomatization' has become more restrictive to correspond
better to internal axioms as singleton facts with mandatory name. Minor
INCOMPATIBILITY.

* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method
definitions.

* Proof method "use" allows to modify the main facts of a given method
expression, e.g.

  (use facts in simp)
  (use facts in \<open>simp add: ...\<close>)

* The old proof method "default" has been removed (legacy since
Isabelle2016). INCOMPATIBILITY, use "standard" instead.


*** Pure ***

* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.

* The command 'unfolding' and proof method "unfold" include a second
stage where given equations are passed through the attribute "abs_def"
before rewriting. This ensures that definitions are fully expanded,
regardless of the actual parameters that are provided. Rare
INCOMPATIBILITY in some corner cases: use proof method (simp only:)
instead, or declare [[unfold_abs_def = false]] in the proof context.

* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
INCOMPATIBILITY, need to provide explicit type constraints for Pure
types where this is really intended.


*** HOL ***

* New proof method "argo" using the built-in Argo solver based on SMT
technology. The method can be used to prove goals of quantifier-free
propositional logic, goals based on a combination of quantifier-free
propositional logic with equality, and goals based on a combination of
quantifier-free propositional logic with linear real arithmetic
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.

* The new "nunchaku" command integrates the Nunchaku model finder. The
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.

* Metis: The problem encoding has changed very slightly. This might
break existing proofs. INCOMPATIBILITY.

* Sledgehammer:
  - The MaSh relevance filter is now faster than before.
  - Produce syntactically correct Vampire 4.0 problem files.

* (Co)datatype package:
  - New commands for defining corecursive functions and reasoning about
    them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
    'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
    method. See 'isabelle doc corec'.
  - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class
    citizen in bounded natural functors.
  - 'primrec' now allows nested calls through the predicator in addition
    to the map function.
  - 'bnf' automatically discharges reflexive proof obligations.
  - 'bnf' outputs a slightly modified proof obligation expressing rel in
       terms of map and set
       (not giving a specification for rel makes this one reflexive).
  - 'bnf' outputs a new proof obligation expressing pred in terms of set
       (not giving a specification for pred makes this one reflexive).
    INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.
  - Renamed lemmas:
      rel_prod_apply ~> rel_prod_inject
      pred_prod_apply ~> pred_prod_inject
    INCOMPATIBILITY.
  - The "size" plugin has been made compatible again with locales.
  - The theorems about "rel" and "set" may have a slightly different (but
    equivalent) form.
    INCOMPATIBILITY.

* The 'coinductive' command produces a proper coinduction rule for
mutual coinductive predicates. This new rule replaces the old rule,
which exposed details of the internal fixpoint construction and was
hard to use. INCOMPATIBILITY.

* New abbreviations for negated existence (but not bounded existence):

  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)

* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
has been removed for output. It is retained for input only, until it is
eliminated altogether.

* The unique existence quantifier no longer provides 'binder' syntax,
but uses syntax translations (as for bounded unique existence). Thus
iterated quantification \<exists>!x y. P x y with its slightly confusing
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
INCOMPATIBILITY in rare situations.

* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
INCOMPATIBILITY.

* Renamed constants and corresponding theorems:

    setsum ~> sum
    setprod ~> prod
    listsum ~> sum_list
    listprod ~> prod_list

INCOMPATIBILITY.

* Sligthly more standardized theorem names:
    sgn_times ~> sgn_mult
    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
    divide_zero_left ~> div_0
    zero_mod_left ~> mod_0
    divide_zero ~> div_by_0
    divide_1 ~> div_by_1
    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
    mod_div_equality ~> div_mult_mod_eq
    mod_div_equality2 ~> mult_div_mod_eq
    mod_div_equality3 ~> mod_div_mult_eq
    mod_div_equality4 ~> mod_mult_div_eq
    minus_div_eq_mod ~> minus_div_mult_eq_mod
    minus_div_eq_mod2 ~> minus_mult_div_eq_mod
    minus_mod_eq_div ~> minus_mod_eq_div_mult
    minus_mod_eq_div2 ~> minus_mod_eq_mult_div
    div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
    mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    div_1 ~> div_by_Suc_0
    mod_1 ~> mod_by_Suc_0
INCOMPATIBILITY.

* New type class "idom_abs_sgn" specifies algebraic properties
of sign and absolute value functions.  Type class "sgn_if" has
disappeared.  Slight INCOMPATIBILITY.

* Dedicated syntax LENGTH('a) for length of types.

* Characters (type char) are modelled as finite algebraic type
corresponding to {0..255}.

  - Logical representation:
    * 0 is instantiated to the ASCII zero character.
    * All other characters are represented as "Char n"
      with n being a raw numeral expression less than 256.
    * Expressions of the form "Char n" with n greater than 255
      are non-canonical.
  - Printing and parsing:
    * Printable characters are printed and parsed as "CHR ''\<dots>''"
      (as before).
    * The ASCII zero character is printed and parsed as "0".
    * All other canonical characters are printed as "CHR 0xXX"
      with XX being the hexadecimal character code.  "CHR n"
      is parsable for every numeral expression n.
    * Non-canonical characters have no special syntax and are
      printed as their logical representation.
  - Explicit conversions from and to the natural numbers are
    provided as char_of_nat, nat_of_char (as before).
  - The auxiliary nibble type has been discontinued.

INCOMPATIBILITY.

* Type class "div" with operation "mod" renamed to type class "modulo"
with operation "modulo", analogously to type class "divide". This
eliminates the need to qualify any of those names in the presence of
infix "mod" syntax. INCOMPATIBILITY.

* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
have been clarified. The fixpoint properties are lfp_fixpoint, its
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
for the proof (lfp_lemma2 etc.) are no longer exported, but can be
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.

* Constant "surj" is a mere input abbreviation, to avoid hiding an
equation in term output. Minor INCOMPATIBILITY.

* Command 'code_reflect' accepts empty constructor lists for datatypes,
which renders those abstract effectively.

* Command 'export_code' checks given constants for abstraction
violations: a small guarantee that given constants specify a safe
interface for the generated code.

* Code generation for Scala: ambiguous implicts in class diagrams are
spelt out explicitly.

* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
explicitly provided auxiliary definitions for required type class
dictionaries rather than half-working magic. INCOMPATIBILITY, see the
tutorial on code generation for details.

* Theory Set_Interval: substantial new theorems on indexed sums and
products.

* Locale bijection establishes convenient default simp rules such as
"inv f (f a) = a" for total bijections.

* Abstract locales semigroup, abel_semigroup, semilattice,
semilattice_neutr, ordering, ordering_top, semilattice_order,
semilattice_neutr_order, comm_monoid_set, semilattice_set,
semilattice_neutr_set, semilattice_order_set,
semilattice_order_neutr_set monoid_list, comm_monoid_list,
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified
syntax uniformly that does not clash with corresponding global syntax.
INCOMPATIBILITY.

* Former locale lifting_syntax is now a bundle, which is easier to
include in a local context or theorem statement, e.g. "context includes
lifting_syntax begin ... end". Minor INCOMPATIBILITY.

* Some old / obsolete theorems have been renamed / removed, potential
INCOMPATIBILITY.

  nat_less_cases  --  removed, use linorder_cases instead
  inv_image_comp  --  removed, use image_inv_f_f instead
  image_surj_f_inv_f  ~>  image_f_inv_f

* Some theorems about groups and orders have been generalised from
  groups to semi-groups that are also monoids:
    le_add_same_cancel1
    le_add_same_cancel2
    less_add_same_cancel1
    less_add_same_cancel2
    add_le_same_cancel1
    add_le_same_cancel2
    add_less_same_cancel1
    add_less_same_cancel2

* Some simplifications theorems about rings have been removed, since
  superseeded by a more general version:
    less_add_cancel_left_greater_zero ~> less_add_same_cancel1
    less_add_cancel_right_greater_zero ~> less_add_same_cancel2
    less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
    less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
    less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
    less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
    less_add_cancel_left_less_zero ~> add_less_same_cancel1
    less_add_cancel_right_less_zero ~> add_less_same_cancel2
INCOMPATIBILITY.

* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.

* Added class topological_monoid.

* The following theorems have been renamed:

  setsum_left_distrib ~> sum_distrib_right
  setsum_right_distrib ~> sum_distrib_left

INCOMPATIBILITY.

* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.

* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `
A)".

* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.

* The type class ordered_comm_monoid_add is now called
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
is introduced as the combination of ordered_ab_semigroup_add +
comm_monoid_add. INCOMPATIBILITY.

* Introduced the type classes canonically_ordered_comm_monoid_add and
dioid.

* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
instantiating linordered_semiring_strict and ordered_ab_group_add, an
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
be required. INCOMPATIBILITY.

* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
  lcm_left_commute_nat ~> lcm.left_commute
  lcm_left_commute_int ~> lcm.left_commute
  gcd_left_commute_nat ~> gcd.left_commute
  gcd_left_commute_int ~> gcd.left_commute
  gcd_greatest_iff_nat ~> gcd_greatest_iff
  gcd_greatest_iff_int ~> gcd_greatest_iff
  coprime_dvd_mult_nat ~> coprime_dvd_mult
  coprime_dvd_mult_int ~> coprime_dvd_mult
  zpower_numeral_even ~> power_numeral_even
  gcd_mult_cancel_nat ~> gcd_mult_cancel
  gcd_mult_cancel_int ~> gcd_mult_cancel
  div_gcd_coprime_nat ~> div_gcd_coprime
  div_gcd_coprime_int ~> div_gcd_coprime
  zpower_numeral_odd ~> power_numeral_odd
  zero_less_int_conv ~> of_nat_0_less_iff
  gcd_greatest_nat ~> gcd_greatest
  gcd_greatest_int ~> gcd_greatest
  coprime_mult_nat ~> coprime_mult
  coprime_mult_int ~> coprime_mult
  lcm_commute_nat ~> lcm.commute
  lcm_commute_int ~> lcm.commute
  int_less_0_conv ~> of_nat_less_0_iff
  gcd_commute_nat ~> gcd.commute
  gcd_commute_int ~> gcd.commute
  Gcd_insert_nat ~> Gcd_insert
  Gcd_insert_int ~> Gcd_insert
  of_int_int_eq ~> of_int_of_nat_eq
  lcm_least_nat ~> lcm_least
  lcm_least_int ~> lcm_least
  lcm_assoc_nat ~> lcm.assoc
  lcm_assoc_int ~> lcm.assoc
  int_le_0_conv ~> of_nat_le_0_iff
  int_eq_0_conv ~> of_nat_eq_0_iff
  Gcd_empty_nat ~> Gcd_empty
  Gcd_empty_int ~> Gcd_empty
  gcd_assoc_nat ~> gcd.assoc
  gcd_assoc_int ~> gcd.assoc
  zero_zle_int ~> of_nat_0_le_iff
  lcm_dvd2_nat ~> dvd_lcm2
  lcm_dvd2_int ~> dvd_lcm2
  lcm_dvd1_nat ~> dvd_lcm1
  lcm_dvd1_int ~> dvd_lcm1
  gcd_zero_nat ~> gcd_eq_0_iff
  gcd_zero_int ~> gcd_eq_0_iff
  gcd_dvd2_nat ~> gcd_dvd2
  gcd_dvd2_int ~> gcd_dvd2
  gcd_dvd1_nat ~> gcd_dvd1
  gcd_dvd1_int ~> gcd_dvd1
  int_numeral ~> of_nat_numeral
  lcm_ac_nat ~> ac_simps
  lcm_ac_int ~> ac_simps
  gcd_ac_nat ~> ac_simps
  gcd_ac_int ~> ac_simps
  abs_int_eq ~> abs_of_nat
  zless_int ~> of_nat_less_iff
  zdiff_int ~> of_nat_diff
  zadd_int ~> of_nat_add
  int_mult ~> of_nat_mult
  int_Suc ~> of_nat_Suc
  inj_int ~> inj_of_nat
  int_1 ~> of_nat_1
  int_0 ~> of_nat_0
  Lcm_empty_nat ~> Lcm_empty
  Lcm_empty_int ~> Lcm_empty
  Lcm_insert_nat ~> Lcm_insert
  Lcm_insert_int ~> Lcm_insert
  comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
  comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
  comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
  comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
  Lcm_eq_0 ~> Lcm_eq_0_I
  Lcm0_iff ~> Lcm_0_iff
  Lcm_dvd_int ~> Lcm_least
  divides_mult_nat ~> divides_mult
  divides_mult_int ~> divides_mult
  lcm_0_nat ~> lcm_0_right
  lcm_0_int ~> lcm_0_right
  lcm_0_left_nat ~> lcm_0_left
  lcm_0_left_int ~> lcm_0_left
  dvd_gcd_D1_nat ~> dvd_gcdD1
  dvd_gcd_D1_int ~> dvd_gcdD1
  dvd_gcd_D2_nat ~> dvd_gcdD2
  dvd_gcd_D2_int ~> dvd_gcdD2
  coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
  coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
  realpow_minus_mult ~> power_minus_mult
  realpow_Suc_le_self ~> power_Suc_le_self
  dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
INCOMPATIBILITY.

* Renamed HOL/Quotient_Examples/FSet.thy to
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.

* Session HOL-Library: theory FinFun bundles "finfun_syntax" and
"no_finfun_syntax" allow to control optional syntax in local contexts;
this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
"unbundle finfun_syntax" to imitate import of
"~~/src/HOL/Library/FinFun_Syntax".

* Session HOL-Library: theory Multiset_Permutations (executably) defines
the set of permutations of a given set or multiset, i.e. the set of all
lists that contain every element of the carrier (multi-)set exactly
once.

* Session HOL-Library: multiset membership is now expressed using
set_mset rather than count.

  - Expressions "count M a > 0" and similar simplify to membership
    by default.

  - Converting between "count M a = 0" and non-membership happens using
    equations count_eq_zero_iff and not_in_iff.

  - Rules count_inI and in_countE obtain facts of the form
    "count M a = n" from membership.

  - Rules count_in_diffI and in_diff_countE obtain facts of the form
    "count M a = n + count N a" from membership on difference sets.

INCOMPATIBILITY.

* Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
displaying equations in functional programming style --- variables
present on the left-hand but not on the righ-hand side are replaced by
underscores.

* Session HOL-Library: theory Combinator_PER provides combinator to
build partial equivalence relations from a predicate and an equivalence
relation.

* Session HOL-Library: theory Perm provides basic facts about almost
everywhere fix bijections.

* Session HOL-Library: theory Normalized_Fraction allows viewing an
element of a field of fractions as a normalized fraction (i.e. a pair of
numerator and denominator such that the two are coprime and the
denominator is normalized wrt. unit factors).

* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.

* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.

* Session HOL-Analysis: measure theory has been moved here from
HOL-Probability. When importing HOL-Analysis some theorems need
additional name spaces prefixes due to name clashes. INCOMPATIBILITY.

* Session HOL-Analysis: more complex analysis including Cauchy's
inequality, Liouville theorem, open mapping theorem, maximum modulus
principle, Residue theorem, Schwarz Lemma.

* Session HOL-Analysis: Theory of polyhedra: faces, extreme points,
polytopes, and the Krein–Milman Minkowski theorem.

* Session HOL-Analysis: Numerous results ported from the HOL Light
libraries: homeomorphisms, continuous function extensions, invariance of
domain.

* Session HOL-Probability: the type of emeasure and nn_integral was
changed from ereal to ennreal, INCOMPATIBILITY.

  emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal
  nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal

* Session HOL-Probability: Code generation and QuickCheck for
Probability Mass Functions.

* Session HOL-Probability: theory Random_Permutations contains some
theory about choosing a permutation of a set uniformly at random and
folding over a list in random order.

* Session HOL-Probability: theory SPMF formalises discrete
subprobability distributions.

* Session HOL-Library: the names of multiset theorems have been
normalised to distinguish which ordering the theorems are about

    mset_less_eqI ~> mset_subset_eqI
    mset_less_insertD ~> mset_subset_insertD
    mset_less_eq_count ~> mset_subset_eq_count
    mset_less_diff_self ~> mset_subset_diff_self
    mset_le_exists_conv ~> mset_subset_eq_exists_conv
    mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
    mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
    mset_le_mono_add ~> mset_subset_eq_mono_add
    mset_le_add_left ~> mset_subset_eq_add_left
    mset_le_add_right ~> mset_subset_eq_add_right
    mset_le_single ~> mset_subset_eq_single
    mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
    diff_le_self ~> diff_subset_eq_self
    mset_leD ~> mset_subset_eqD
    mset_lessD ~> mset_subsetD
    mset_le_insertD ~> mset_subset_eq_insertD
    mset_less_of_empty ~> mset_subset_of_empty
    mset_less_size ~> mset_subset_size
    wf_less_mset_rel ~> wf_subset_mset_rel
    count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
    mset_remdups_le ~> mset_remdups_subset_eq
    ms_lesseq_impl ~> subset_eq_mset_impl

Some functions have been renamed:
    ms_lesseq_impl -> subset_eq_mset_impl

* HOL-Library: multisets are now ordered with the multiset ordering
    #\<subseteq># ~> \<le>
    #\<subset># ~> <
    le_multiset ~> less_eq_multiset
    less_multiset ~> le_multiset
INCOMPATIBILITY.

* Session HOL-Library: the prefix multiset_order has been discontinued:
the theorems can be directly accessed. As a consequence, the lemmas
"order_multiset" and "linorder_multiset" have been discontinued, and the
interpretations "multiset_linorder" and "multiset_wellorder" have been
replaced by instantiations. INCOMPATIBILITY.

* Session HOL-Library: some theorems about the multiset ordering have
been renamed:

    le_multiset_def ~> less_eq_multiset_def
    less_multiset_def ~> le_multiset_def
    less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
    mult_less_not_refl ~> mset_le_not_refl
    mult_less_trans ~> mset_le_trans
    mult_less_not_sym ~> mset_le_not_sym
    mult_less_asym ~> mset_le_asym
    mult_less_irrefl ~> mset_le_irrefl
    union_less_mono2{,1,2} ~> union_le_mono2{,1,2}

    le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
    le_multiset_total ~> less_eq_multiset_total
    less_multiset_right_total ~> subset_eq_imp_le_multiset
    le_multiset_empty_left ~> less_eq_multiset_empty_left
    le_multiset_empty_right ~> less_eq_multiset_empty_right
    less_multiset_empty_right ~> le_multiset_empty_left
    less_multiset_empty_left ~> le_multiset_empty_right
    union_less_diff_plus ~> union_le_diff_plus
    ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
    less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
    le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
INCOMPATIBILITY.

* Session HOL-Library: the lemma mset_map has now the attribute [simp].
INCOMPATIBILITY.

* Session HOL-Library: some theorems about multisets have been removed.
INCOMPATIBILITY, use the following replacements:

    le_multiset_plus_plus_left_iff ~> add_less_cancel_right
    less_multiset_plus_plus_left_iff ~> add_less_cancel_right
    le_multiset_plus_plus_right_iff ~> add_less_cancel_left
    less_multiset_plus_plus_right_iff ~> add_less_cancel_left
    add_eq_self_empty_iff ~> add_cancel_left_right
    mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
    mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
    mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
    empty_inter ~> subset_mset.inf_bot_left
    inter_empty ~> subset_mset.inf_bot_right
    empty_sup ~> subset_mset.sup_bot_left
    sup_empty ~> subset_mset.sup_bot_right
    bdd_below_multiset ~> subset_mset.bdd_above_bot
    subset_eq_empty ~> subset_mset.le_zero_eq
    le_empty ~> subset_mset.le_zero_eq
    mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
    mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero

* Session HOL-Library: some typeclass constraints about multisets have
been reduced from ordered or linordered to preorder. Multisets have the
additional typeclasses order_bot, no_top,
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
linordered_cancel_ab_semigroup_add, and
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.

* Session HOL-Library: there are some new simplification rules about
multisets, the multiset ordering, and the subset ordering on multisets.
INCOMPATIBILITY.

* Session HOL-Library: the subset ordering on multisets has now the
interpretations ordered_ab_semigroup_monoid_add_imp_le and
bounded_lattice_bot. INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: single has been removed in favor
of add_mset that roughly corresponds to Set.insert. Some theorems have
removed or changed:

  single_not_empty ~> add_mset_not_empty or empty_not_add_mset
  fold_mset_insert ~> fold_mset_add_mset
  image_mset_insert ~> image_mset_add_mset
  union_single_eq_diff
  multi_self_add_other_not_self
  diff_single_eq_union
INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: some theorems have been changed
to use add_mset instead of single:

  mset_add
  multi_self_add_other_not_self
  diff_single_eq_union
  union_single_eq_diff
  union_single_eq_member
  add_eq_conv_diff
  insert_noteq_member
  add_eq_conv_ex
  multi_member_split
  multiset_add_sub_el_shuffle
  mset_subset_eq_insertD
  mset_subset_insertD
  insert_subset_eq_iff
  insert_union_subset_iff
  multi_psub_of_add_self
  inter_add_left1
  inter_add_left2
  inter_add_right1
  inter_add_right2
  sup_union_left1
  sup_union_left2
  sup_union_right1
  sup_union_right2
  size_eq_Suc_imp_eq_union
  multi_nonempty_split
  mset_insort
  mset_update
  mult1I
  less_add
  mset_zip_take_Cons_drop_twice
  rel_mset_Zero
  msed_map_invL
  msed_map_invR
  msed_rel_invL
  msed_rel_invR
  le_multiset_right_total
  multiset_induct
  multiset_induct2_size
  multiset_induct2
INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: the definitions of some
constants have changed to use add_mset instead of adding a single
element:

  image_mset
  mset
  replicate_mset
  mult1
  pred_mset
  rel_mset'
  mset_insort

INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: due to the above changes, the
attributes of some multiset theorems have been changed:

  insert_DiffM  [] ~> [simp]
  insert_DiffM2 [simp] ~> []
  diff_add_mset_swap [simp]
  fold_mset_add_mset [simp]
  diff_diff_add [simp] (for multisets only)
  diff_cancel [simp] ~> []
  count_single [simp] ~> []
  set_mset_single [simp] ~> []
  size_multiset_single [simp] ~> []
  size_single [simp] ~> []
  image_mset_single [simp] ~> []
  mset_subset_eq_mono_add_right_cancel [simp] ~> []
  mset_subset_eq_mono_add_left_cancel [simp] ~> []
  fold_mset_single [simp] ~> []
  subset_eq_empty [simp] ~> []
  empty_sup [simp] ~> []
  sup_empty [simp] ~> []
  inter_empty [simp] ~> []
  empty_inter [simp] ~> []
INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: the order of the variables in
the second cases of multiset_induct, multiset_induct2_size,
multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: there is now a simplification
procedure on multisets. It mimics the behavior of the procedure on
natural numbers. INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: renamed sums and products of
multisets:

  msetsum ~> sum_mset
  msetprod ~> prod_mset

* Session HOL-Library, theory Multiset: the notation for intersection
and union of multisets have been changed:

  #\<inter> ~> \<inter>#
  #\<union> ~> \<union>#

INCOMPATIBILITY.

* Session HOL-Library, theory Multiset: the lemma
one_step_implies_mult_aux on multisets has been removed, use
one_step_implies_mult instead. INCOMPATIBILITY.

* Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
support for monotonicity and continuity in chain-complete partial orders
and about admissibility conditions for fixpoint inductions.

* Session HOL-Library: theory Library/Polynomial contains also
derivation of polynomials (formerly in Library/Poly_Deriv) but not
gcd/lcm on polynomials over fields. This has been moved to a separate
theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
future different type class instantiation for polynomials over factorial
rings. INCOMPATIBILITY.

* Session HOL-Library: theory Sublist provides function "prefixes" with
the following renaming

  prefixeq -> prefix
  prefix -> strict_prefix
  suffixeq -> suffix
  suffix -> strict_suffix

Added theory of longest common prefixes.

* Session HOL-Number_Theory: algebraic foundation for primes:
Generalisation of predicate "prime" and introduction of predicates
"prime_elem", "irreducible", a "prime_factorization" function, and the
"factorial_ring" typeclass with instance proofs for nat, int, poly. Some
theorems now have different names, most notably "prime_def" is now
"prime_nat_iff". INCOMPATIBILITY.

* Session Old_Number_Theory has been removed, after porting remaining
theories.

* Session HOL-Types_To_Sets provides an experimental extension of
Higher-Order Logic to allow translation of types to sets.


*** ML ***

* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
library (notably for big integers). Subtle change of semantics:
Integer.gcd and Integer.lcm both normalize the sign, results are never
negative. This coincides with the definitions in HOL/GCD.thy.
INCOMPATIBILITY.

* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.

* ML antiquotation @{path} is superseded by @{file}, which ensures that
the argument is a plain file. Minor INCOMPATIBILITY.

* Antiquotation @{make_string} is available during Pure bootstrap --
with approximative output quality.

* Low-level ML system structures (like PolyML and RunCall) are no longer
exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.

* The ML function "ML" provides easy access to run-time compilation.
This is particularly useful for conditional compilation, without
requiring separate files.

* Option ML_exception_debugger controls detailed exception trace via the
Poly/ML debugger. Relevant ML modules need to be compiled beforehand
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
debugger information requires consirable time and space: main
Isabelle/HOL with full debugger support may need ML_system_64.

* Local_Theory.restore has been renamed to Local_Theory.reset to
emphasize its disruptive impact on the cumulative context, notably the
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
only appropriate when targets are managed, e.g. starting from a global
theory and returning to it. Regular definitional packages should use
balanced blocks of Local_Theory.open_target versus
Local_Theory.close_target instead. Rare INCOMPATIBILITY.

* Structure TimeLimit (originally from the SML/NJ library) has been
replaced by structure Timeout, with slightly different signature.
INCOMPATIBILITY.

* Discontinued cd and pwd operations, which are not well-defined in a
multi-threaded environment. Note that files are usually located
relatively to the master directory of a theory (see also
File.full_path). Potential INCOMPATIBILITY.

* Binding.empty_atts supersedes Thm.empty_binding and
Attrib.empty_binding. Minor INCOMPATIBILITY.


*** System ***

* SML/NJ and old versions of Poly/ML are no longer supported.

* Poly/ML heaps now follow the hierarchy of sessions, and thus require
much less disk space.

* The Isabelle ML process is now managed directly by Isabelle/Scala, and
shell scripts merely provide optional command-line access. In
particular:

  . Scala module ML_Process to connect to the raw ML process,
    with interaction via stdin/stdout/stderr or in batch mode;
  . command-line tool "isabelle console" as interactive wrapper;
  . command-line tool "isabelle process" as batch mode wrapper.

* The executable "isabelle_process" has been discontinued. Tools and
prover front-ends should use ML_Process or Isabelle_Process in
Isabelle/Scala. INCOMPATIBILITY.

* New command-line tool "isabelle process" supports ML evaluation of
literal expressions (option -e) or files (option -f) in the context of a
given heap image. Errors lead to premature exit of the ML process with
return code 1.

* The command-line tool "isabelle build" supports option -N for cyclic
shuffling of NUMA CPU nodes. This may help performance tuning on Linux
servers with separate CPU/memory modules.

* System option "threads" (for the size of the Isabelle/ML thread farm)
is also passed to the underlying ML runtime system as --gcthreads,
unless there is already a default provided via ML_OPTIONS settings.

* System option "checkpoint" helps to fine-tune the global heap space
management of isabelle build. This is relevant for big sessions that may
exhaust the small 32-bit address space of the ML process (which is used
by default).

* System option "profiling" specifies the mode for global ML profiling
in "isabelle build". Possible values are "time", "allocations". The
command-line tool "isabelle profiling_report" helps to digest the
resulting log files.

* System option "ML_process_policy" specifies an optional command prefix
for the underlying ML process, e.g. to control CPU affinity on
multiprocessor systems. The "isabelle jedit" tool allows to override the
implicit default via option -p.

* Command-line tool "isabelle console" provides option -r to help to
bootstrapping Isabelle/Pure interactively.

* Command-line tool "isabelle yxml" has been discontinued.
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
Isabelle/ML or Isabelle/Scala.

* Many Isabelle tools that require a Java runtime system refer to the
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
depending on the underlying platform. The settings for "isabelle build"
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
discontinued. Potential INCOMPATIBILITY.

* The Isabelle system environment always ensures that the main
executables are found within the shell search $PATH: "isabelle" and
"isabelle_scala_script".

* Isabelle tools may consist of .scala files: the Scala compiler is
invoked on the spot. The source needs to define some object that extends
Isabelle_Tool.Body.