Isabelle NEWS -- history of user-relevant changes

 =================================================

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

 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.

 (* hint by Makarius how to introduce templates, referring to

  http://isabelle.in.tum.de/repos/isabelle/rev/9f8d06f23c09 

  Here Output.information writes to respective window.

  Isac needs output into main window, probably as done by metis.

 *)

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

 * File.bash_string, File.bash_path etc. represent Isabelle/ML and

 Isabelle/Scala strings authentically within GNU bash. This is useful to

 produce robust shell scripts under program control, without worrying

 about spaces or special characters. Note that user output works via

 Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and

 less versatile) operations File.shell_quote, File.shell_path etc. have

 been discontinued.

 * The isabelle_java executable allows to run a Java process within the

 name space of Java and Scala components that are bundled with Isabelle,

 but without the Isabelle settings environment.

 * Isabelle/Scala: the SSH module supports ssh and sftp connections, for

 remote command-execution and file-system access. This resembles

 operations from module File and Isabelle_System to some extent. Note

 that Path specifications need to be resolved remotely via

 ssh.remote_path instead of File.standard_path: the implicit process

 environment is different, Isabelle settings are not available remotely.

 * Isabelle/Scala: the Mercurial module supports repositories via the

 regular hg command-line interface. The repositroy clone and working

 directory may reside on a local or remote file-system (via ssh

 connection).

 New in Isabelle2016 (February 2016)

 -----------------------------------

 *** General ***

 * Eisbach is now based on Pure instead of HOL. Objects-logics may import

 either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or

 ~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that

 the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further

 examples that do require HOL.

 * Better resource usage on all platforms (Linux, Windows, Mac OS X) for

 both Isabelle/ML and Isabelle/Scala.  Slightly reduced heap space usage.

 * Former "xsymbols" syntax with Isabelle symbols is used by default,

 without any special print mode. Important ASCII replacement syntax

 remains available under print mode "ASCII", but less important syntax

 has been removed (see below).

 * Support for more arrow symbols, with rendering in LaTeX and Isabelle

 fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.

 * Special notation \<struct> for the first implicit 'structure' in the

 context has been discontinued. Rare INCOMPATIBILITY, use explicit

 structure name instead, notably in indexed notation with block-subscript

 (e.g. \<odot>\<^bsub>A\<^esub>).

 * The glyph for \<diamond> in the IsabelleText font now corresponds better to its

 counterpart \<box> as quantifier-like symbol. A small diamond is available as

 \<diamondop>; the old symbol \<struct> loses this rendering and any special

 meaning.

 * Syntax for formal comments "-- text" now also supports the symbolic

 form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps

 to update old sources.

 * Toplevel theorem statements have been simplified as follows:

   theorems             ~>  lemmas

   schematic_lemma      ~>  schematic_goal

   schematic_theorem    ~>  schematic_goal

   schematic_corollary  ~>  schematic_goal

 Command-line tool "isabelle update_theorems" updates theory sources

 accordingly.

 * Toplevel theorem statement 'proposition' is another alias for

 'theorem'.

 * The old 'defs' command has been removed (legacy since Isabelle2014).

 INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or

 deferred definitions require a surrounding 'overloading' block.

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

 * IDE support for the source-level debugger of Poly/ML, to work with

 Isabelle/ML and official Standard ML. Option "ML_debugger" and commands

 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',

 'SML_file_no_debug' control compilation of sources with or without

 debugging information. The Debugger panel allows to set breakpoints (via

 context menu), step through stopped threads, evaluate local ML

 expressions etc. At least one Debugger view needs to be active to have

 any effect on the running ML program.

 * The State panel manages explicit proof state output, with dynamic

 auto-update according to cursor movement. Alternatively, the jEdit

 action "isabelle.update-state" (shortcut S+ENTER) triggers manual

 update.

 * The Output panel no longer shows proof state output by default, to

 avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or

 enable option "editor_output_state".

 * The text overview column (status of errors, warnings etc.) is updated

 asynchronously, leading to much better editor reactivity. Moreover, the

 full document node content is taken into account. The width of the

 column is scaled according to the main text area font, for improved

 visibility.

 * The main text area no longer changes its color hue in outdated

 situations. The text overview column takes over the role to indicate

 unfinished edits in the PIDE pipeline. This avoids flashing text display

 due to ad-hoc updates by auxiliary GUI components, such as the State

 panel.

 * Slightly improved scheduling for urgent print tasks (e.g. command

 state output, interactive queries) wrt. long-running background tasks.

 * Completion of symbols via prefix of \<name> or \<^name> or \name is

 always possible, independently of the language context. It is never

 implicit: a popup will show up unconditionally.

 * Additional abbreviations for syntactic completion may be specified in

 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with

 support for simple templates using ASCII 007 (bell) as placeholder.

 * Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for

 completion like "+o", "*o", ".o" etc. -- due to conflicts with other

 ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define

 suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.

 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls

 emphasized text style; the effect is visible in document output, not in

 the editor.

 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,

 instead of former C+e LEFT.

 * The command-line tool "isabelle jedit" and the isabelle.Main

 application wrapper treat the default $USER_HOME/Scratch.thy more

 uniformly, and allow the dummy file argument ":" to open an empty buffer

 instead.

 * New command-line tool "isabelle jedit_client" allows to connect to an

 already running Isabelle/jEdit process. This achieves the effect of

 single-instance applications seen on common GUI desktops.

 * The default look-and-feel for Linux is the traditional "Metal", which

 works better with GUI scaling for very high-resolution displays (e.g.

 4K). Moreover, it is generally more robust than "Nimbus".

 * Update to jedit-5.3.0, with improved GUI scaling and support of

 high-resolution displays (e.g. 4K).

 * The main Isabelle executable is managed as single-instance Desktop

 application uniformly on all platforms: Linux, Windows, Mac OS X.

 *** Document preparation ***

 * Commands 'paragraph' and 'subparagraph' provide additional section

 headings. Thus there are 6 levels of standard headings, as in HTML.

 * Command 'text_raw' has been clarified: input text is processed as in

 'text' (with antiquotations and control symbols). The key difference is

 the lack of the surrounding isabelle markup environment in output.

 * Text is structured in paragraphs and nested lists, using notation that

 is similar to Markdown. The control symbols for list items are as

 follows:

   \<^item>  itemize

   \<^enum>  enumerate

   \<^descr>  description

 * There is a new short form for antiquotations with a single argument

 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and

 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.

 \<^name> without following cartouche is equivalent to @{name}. The

 standard Isabelle fonts provide glyphs to render important control

 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".

 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with

 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using

 standard LaTeX macros of the same names.

 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.

 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal

 text. Command-line tool "isabelle update_cartouches -t" helps to update

 old sources, by approximative patching of the content of string and

 cartouche tokens seen in theory sources.

 * The @{text} antiquotation now ignores the antiquotation option

 "source". The given text content is output unconditionally, without any

 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the

 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial

 or terminal spaces are ignored.

 * Antiquotations @{emph} and @{bold} output LaTeX source recursively,

 adding appropriate text style markup. These may be used in the short

 form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.

 * Document antiquotation @{footnote} outputs LaTeX source recursively,

 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.

 * Antiquotation @{verbatim [display]} supports option "indent".

 * Antiquotation @{theory_text} prints uninterpreted theory source text

 (Isar outer syntax with command keywords etc.). This may be used in the

 short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".

 * Antiquotation @{doc ENTRY} provides a reference to the given

 documentation, with a hyperlink in the Prover IDE.

 * Antiquotations @{command}, @{method}, @{attribute} print checked

 entities of the Isar language.

 * HTML presentation uses the standard IsabelleText font and Unicode

 rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former

 print mode "HTML" loses its special meaning.

 *** Isar ***

 * Local goals ('have', 'show', 'hence', 'thus') allow structured rule

 statements like fixes/assumes/shows in theorem specifications, but the

 notation is postfix with keywords 'if' (or 'when') and 'for'. For

 example:

   have result: "C x y"

     if "A x" and "B y"

     for x :: 'a and y :: 'a

     <proof>

 The local assumptions are bound to the name "that". The result is

 exported from context of the statement as usual. The above roughly

 corresponds to a raw proof block like this:

   {

     fix x :: 'a and y :: 'a

     assume that: "A x" "B y"

     have "C x y" <proof>

   }

   note result = this

 The keyword 'when' may be used instead of 'if', to indicate 'presume'

 instead of 'assume' above.

 * Assumptions ('assume', 'presume') allow structured rule statements

 using 'if' and 'for', similar to 'have' etc. above. For example:

   assume result: "C x y"

     if "A x" and "B y"

     for x :: 'a and y :: 'a

 This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general

 result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".

 Vacuous quantification in assumptions is omitted, i.e. a for-context

 only effects propositions according to actual use of variables. For

 example:

   assume "A x" and "B y" for x and y

 is equivalent to:

   assume "\<And>x. A x" and "\<And>y. B y"

 * The meaning of 'show' with Pure rule statements has changed: premises

 are treated in the sense of 'assume', instead of 'presume'. This means,

 a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as

 follows:

   show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

 or:

   show "C x" if "A x" "B x" for x

 Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

   show "C x" when "A x" "B x" for x

 * New command 'consider' states rules for generalized elimination and

 case splitting. This is like a toplevel statement "theorem obtains" used

 within a proof body; or like a multi-branch 'obtain' without activation

 of the local context elements yet.

 * Proof method "cases" allows to specify the rule as first entry of

 chained facts.  This is particularly useful with 'consider':

   consider (a) A | (b) B | (c) C <proof>

   then have something

   proof cases

     case a

     then show ?thesis <proof>

   next

     case b

     then show ?thesis <proof>

   next

     case c

     then show ?thesis <proof>

   qed

 * Command 'case' allows fact name and attribute specification like this:

   case a: (c xs)

   case a [attributes]: (c xs)

 Facts that are introduced by invoking the case context are uniformly

 qualified by "a"; the same name is used for the cumulative fact. The old

 form "case (c xs) [attributes]" is no longer supported. Rare

 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,

 and always put attributes in front.

 * The standard proof method of commands 'proof' and '..' is now called

 "standard" to make semantically clear what it is; the old name "default"

 is still available as legacy for some time. Documentation now explains

 '..' more accurately as "by standard" instead of "by rule".

 * Nesting of Isar goal structure has been clarified: the context after

 the initial backwards refinement is retained for the whole proof, within

 all its context sections (as indicated via 'next'). This is e.g.

 relevant for 'using', 'including', 'supply':

   have "A \<and> A" if a: A for A

     supply [simp] = a

   proof

     show A by simp

   next

     show A by simp

   qed

 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the

 proof body as well, abstracted over relevant parameters.

 * Improved type-inference for theorem statement 'obtains': separate

 parameter scope for of each clause.

 * Term abbreviations via 'is' patterns also work for schematic

 statements: result is abstracted over unknowns.

 * Command 'subgoal' allows to impose some structure on backward

 refinements, to avoid proof scripts degenerating into long of 'apply'

 sequences. Further explanations and examples are given in the isar-ref

 manual.

 * Command 'supply' supports fact definitions during goal refinement

 ('apply' scripts).

 * Proof method "goal_cases" turns the current subgoals into cases within

 the context; the conclusion is bound to variable ?case in each case. For

 example:

 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

 proof goal_cases

   case (1 x)

   then show ?case using \<open>A x\<close> \<open>B x\<close> sorry

 next

   case (2 y z)

   then show ?case using \<open>U y\<close> \<open>V z\<close> sorry

 qed

 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

 proof goal_cases

   case prems: 1

   then show ?case using prems sorry

 next

   case prems: 2

   then show ?case using prems sorry

 qed

 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.

 is marked as legacy, and will be removed eventually. The proof method

 "goals" achieves a similar effect within regular Isar; often it can be

 done more adequately by other means (e.g. 'consider').

 * The vacuous fact "TERM x" may be established "by fact" or as `TERM x`

 as well, not just "by this" or "." as before.

 * Method "sleep" succeeds after a real-time delay (in seconds). This is

 occasionally useful for demonstration and testing purposes.

 *** Pure ***

 * Qualifiers in locale expressions default to mandatory ('!') regardless

 of the command. Previously, for 'locale' and 'sublocale' the default was

 optional ('?'). The old synatx '!' has been discontinued.

 INCOMPATIBILITY, remove '!' and add '?' as required.

 * Keyword 'rewrites' identifies rewrite morphisms in interpretation

 commands. Previously, the keyword was 'where'. INCOMPATIBILITY.

 * More gentle suppression of syntax along locale morphisms while

 printing terms. Previously 'abbreviation' and 'notation' declarations

 would be suppressed for morphisms except term identity. Now

 'abbreviation' is also kept for morphims that only change the involved

 parameters, and only 'notation' is suppressed. This can be of great help

 when working with complex locale hierarchies, because proof states are

 displayed much more succinctly. It also means that only notation needs

 to be redeclared if desired, as illustrated by this example:

   locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)

   begin

     definition derived (infixl "\<odot>" 65) where ...

   end

   locale morphism =

     left: struct composition + right: struct composition'

     for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)

   begin

     notation right.derived ("\<odot>''")

   end

 * Command 'global_interpretation' issues interpretations into global

 theories, with optional rewrite definitions following keyword 'defines'.

 * Command 'sublocale' accepts optional rewrite definitions after keyword

 'defines'.

 * Command 'permanent_interpretation' has been discontinued. Use

 'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.

 * Command 'print_definitions' prints dependencies of definitional

 specifications. This functionality used to be part of 'print_theory'.

 * Configuration option rule_insts_schematic has been discontinued

 (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.

 * Abbreviations in type classes now carry proper sort constraint. Rare

 INCOMPATIBILITY in situations where the previous misbehaviour has been

 exploited.

 * Refinement of user-space type system in type classes: pseudo-local

 operations behave more similar to abbreviations. Potential

 INCOMPATIBILITY in exotic situations.

 *** HOL ***

 * The 'typedef' command has been upgraded from a partially checked

 "axiomatization", to a full definitional specification that takes the

 global collection of overloaded constant / type definitions into

 account. Type definitions with open dependencies on overloaded

 definitions need to be specified as "typedef (overloaded)". This

 provides extra robustness in theory construction. Rare INCOMPATIBILITY.

 * Qualification of various formal entities in the libraries is done more

 uniformly via "context begin qualified definition ... end" instead of

 old-style "hide_const (open) ...". Consequently, both the defined

 constant and its defining fact become qualified, e.g. Option.is_none and

 Option.is_none_def. Occasional INCOMPATIBILITY in applications.

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

   notation iff  (infixr "<->" 25)

   notation Times  (infixr "<*>" 80)

   type_notation Map.map  (infixr "~=>" 0)

   notation Map.map_comp  (infixl "o'_m" 55)

   type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

   notation FuncSet.funcset  (infixr "->" 60)

   notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)

   notation Omega_Words_Fun.conc (infixr "conc" 65)

   notation Preorder.equiv ("op ~~")

     and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

   notation (in topological_space) tendsto (infixr "--->" 55)

   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)

   notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)

   notation NSA.approx (infixl "@=" 50)

   notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)

   notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)

 * The alternative notation "\<Colon>" for type and sort constraints has been

 removed: in LaTeX document output it looks the same as "::".

 INCOMPATIBILITY, use plain "::" instead.

 * Commands 'inductive' and 'inductive_set' work better when names for

 intro rules are omitted: the "cases" and "induct" rules no longer

 declare empty case_names, but no case_names at all. This allows to use

 numbered cases in proofs, without requiring method "goal_cases".

 * Inductive definitions ('inductive', 'coinductive', etc.) expose

 low-level facts of the internal construction only if the option

 "inductive_internals" is enabled. This refers to the internal predicate

 definition and its monotonicity result. Rare INCOMPATIBILITY.

 * Recursive function definitions ('fun', 'function', 'partial_function')

 expose low-level facts of the internal construction only if the option

 "function_internals" is enabled. Its internal inductive definition is

 also subject to "inductive_internals". Rare INCOMPATIBILITY.

 * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts

 of the internal construction only if the option "bnf_internals" is

 enabled. This supersedes the former option "bnf_note_all". Rare

 INCOMPATIBILITY.

 * Combinator to represent case distinction on products is named

 "case_prod", uniformly, discontinuing any input aliasses. Very popular

 theorem aliasses have been retained.

 Consolidated facts:

   PairE ~> prod.exhaust

   Pair_eq ~> prod.inject

   pair_collapse ~> prod.collapse

   Pair_fst_snd_eq ~> prod_eq_iff

   split_twice ~> prod.case_distrib

   split_weak_cong ~> prod.case_cong_weak

   split_split ~> prod.split

   split_split_asm ~> prod.split_asm

   splitI ~> case_prodI

   splitD ~> case_prodD

   splitI2 ~> case_prodI2

   splitI2' ~> case_prodI2'

   splitE ~> case_prodE

   splitE' ~> case_prodE'

   split_pair ~> case_prod_Pair

   split_eta ~> case_prod_eta

   split_comp ~> case_prod_comp

   mem_splitI ~> mem_case_prodI

   mem_splitI2 ~> mem_case_prodI2

   mem_splitE ~> mem_case_prodE

   The_split ~> The_case_prod

   cond_split_eta ~> cond_case_prod_eta

   Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE

   Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI

   in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq

   Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD

   Collect_split_Grp_inD ~> Collect_case_prod_Grp_in

   Domain_Collect_split ~> Domain_Collect_case_prod

   Image_Collect_split ~> Image_Collect_case_prod

   Range_Collect_split ~> Range_Collect_case_prod

   Eps_split ~> Eps_case_prod

   Eps_split_eq ~> Eps_case_prod_eq

   split_rsp ~> case_prod_rsp

   curry_split ~> curry_case_prod

   split_curry ~> case_prod_curry

 Changes in structure HOLogic:

   split_const ~> case_prod_const

   mk_split ~> mk_case_prod

   mk_psplits ~> mk_ptupleabs

   strip_psplits ~> strip_ptupleabs

 INCOMPATIBILITY.

 * The coercions to type 'real' have been reorganised. The function

 'real' is no longer overloaded, but has type 'nat => real' and

 abbreviates of_nat for that type. Also 'real_of_int :: int => real'

 abbreviates of_int for that type. Other overloaded instances of 'real'

 have been replaced by 'real_of_ereal' and 'real_of_float'.

 Consolidated facts (among others):

   real_of_nat_le_iff -> of_nat_le_iff

   real_of_nat_numeral of_nat_numeral

   real_of_int_zero of_int_0

   real_of_nat_zero of_nat_0

   real_of_one of_int_1

   real_of_int_add of_int_add

   real_of_nat_add of_nat_add

   real_of_int_diff of_int_diff

   real_of_nat_diff of_nat_diff

   floor_subtract floor_diff_of_int

   real_of_int_inject of_int_eq_iff

   real_of_int_gt_zero_cancel_iff of_int_0_less_iff

   real_of_int_ge_zero_cancel_iff of_int_0_le_iff

   real_of_nat_ge_zero of_nat_0_le_iff

   real_of_int_ceiling_ge le_of_int_ceiling

   ceiling_less_eq ceiling_less_iff

   ceiling_le_eq ceiling_le_iff

   less_floor_eq less_floor_iff

   floor_less_eq floor_less_iff

   floor_divide_eq_div floor_divide_of_int_eq

   real_of_int_zero_cancel of_nat_eq_0_iff

   ceiling_real_of_int ceiling_of_int

 INCOMPATIBILITY.

 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has

 been removed. INCOMPATIBILITY.

 * Quickcheck setup for finite sets.

 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.

 * Sledgehammer:

   - The MaSh relevance filter has been sped up.

   - Proof reconstruction has been improved, to minimize the incidence of

     cases where Sledgehammer gives a proof that does not work.

   - Auto Sledgehammer now minimizes and preplays the results.

   - Handle Vampire 4.0 proof output without raising exception.

   - Eliminated "MASH" environment variable. Use the "MaSh" option in

     Isabelle/jEdit instead. INCOMPATIBILITY.

   - Eliminated obsolete "blocking" option and related subcommands.

 * Nitpick:

   - Fixed soundness bug in translation of "finite" predicate.

   - Fixed soundness bug in "destroy_constrs" optimization.

   - Fixed soundness bug in translation of "rat" type.

   - Removed "check_potential" and "check_genuine" options.

   - Eliminated obsolete "blocking" option.

 * (Co)datatype package:

   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF

     structure on the raw type to an abstract type defined using typedef.

   - Always generate "case_transfer" theorem.

   - For mutual types, generate slightly stronger "rel_induct",

     "rel_coinduct", and "coinduct" theorems. INCOMPATIBILITY.

   - Allow discriminators and selectors with the same name as the type

     being defined.

   - Avoid various internal name clashes (e.g., 'datatype f = f').

 * Transfer: new methods for interactive debugging of 'transfer' and

 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',

 'transfer_prover_start' and 'transfer_prover_end'.

 * New diagnostic command print_record for displaying record definitions.

 * Division on integers is bootstrapped directly from division on

 naturals and uses generic numeral algorithm for computations. Slight

 INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former

 simprocs binary_int_div and binary_int_mod

 * Tightened specification of class semiring_no_zero_divisors. Minor

 INCOMPATIBILITY.

 * Class algebraic_semidom introduces common algebraic notions of

 integral (semi)domains, particularly units. Although logically subsumed

 by fields, is is not a super class of these in order not to burden

 fields with notions that are trivial there.

 * Class normalization_semidom specifies canonical representants for

 equivalence classes of associated elements in an integral (semi)domain.

 This formalizes associated elements as well.

 * Abstract specification of gcd/lcm operations in classes semiring_gcd,

 semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute

 and gcd_int.commute are subsumed by gcd.commute, as well as

 gcd_nat.assoc and gcd_int.assoc by gcd.assoc.

 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) are

 logically unified to Rings.divide in syntactic type class Rings.divide,

 with infix syntax (_ div _). Infix syntax (_ / _) for field division is

 added later as abbreviation in class Fields.inverse. INCOMPATIBILITY,

 instantiations must refer to Rings.divide rather than the former

 separate constants, hence infix syntax (_ / _) is usually not available

 during instantiation.

 * New cancellation simprocs for boolean algebras to cancel complementary

 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to

 "top". INCOMPATIBILITY.

 * Class uniform_space introduces uniform spaces btw topological spaces

 and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be

 introduced in the form of an uniformity. Some constants are more general

 now, it may be necessary to add type class constraints.

   open_real_def \<leadsto> open_dist

   open_complex_def \<leadsto> open_dist

 * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.

 * Library/Multiset:

   - Renamed multiset inclusion operators:

       < ~> <#

       > ~> >#

       <= ~> <=#

       >= ~> >=#

       \<le> ~> \<le>#

       \<ge> ~> \<ge>#

     INCOMPATIBILITY.

   - Added multiset inclusion operator syntax:

       \<subset>#

       \<subseteq>#

       \<supset>#

       \<supseteq>#

   - "'a multiset" is no longer an instance of the "order",

     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",

     "semilattice_inf", and "semilattice_sup" type classes. The theorems

     previously provided by these type classes (directly or indirectly)

     are now available through the "subset_mset" interpretation

     (e.g. add_mono ~> subset_mset.add_mono).

     INCOMPATIBILITY.

   - Renamed conversions:

       multiset_of ~> mset

       multiset_of_set ~> mset_set

       set_of ~> set_mset

     INCOMPATIBILITY

   - Renamed lemmas:

       mset_le_def ~> subseteq_mset_def

       mset_less_def ~> subset_mset_def

       less_eq_multiset.rep_eq ~> subseteq_mset_def

     INCOMPATIBILITY

   - Removed lemmas generated by lift_definition:

     less_eq_multiset.abs_eq, less_eq_multiset.rsp,

     less_eq_multiset.transfer, less_eq_multiset_def

     INCOMPATIBILITY

 * Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.

 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the

 Bourbaki-Witt fixpoint theorem for increasing functions in

 chain-complete partial orders.

 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.

 Minor INCOMPATIBILITY, use 'function' instead.

 * Library/Periodic_Fun: a locale that provides convenient lemmas for

 periodic functions.

 * Library/Formal_Power_Series: proper definition of division (with

 remainder) for formal power series; instances for Euclidean Ring and

 GCD.

 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.

 * HOL-Statespace: command 'statespace' uses mandatory qualifier for

 import of parent, as for general 'locale' expressions. INCOMPATIBILITY,

 remove '!' and add '?' as required.

 * HOL-Decision_Procs: The "approximation" method works with "powr"

 (exponentiation on real numbers) again.

 * HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour

 integrals (= complex path integrals), Cauchy's integral theorem, winding

 numbers and Cauchy's integral formula, Liouville theorem, Fundamental

 Theorem of Algebra. Ported from HOL Light.

 * HOL-Multivariate_Analysis: topological concepts such as connected

 components, homotopic paths and the inside or outside of a set.

 * HOL-Multivariate_Analysis: radius of convergence of power series and

 various summability tests; Harmonic numbers and the Euler–Mascheroni

 constant; the Generalised Binomial Theorem; the complex and real

 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important

 properties.

 * HOL-Probability: The central limit theorem based on Levy's uniqueness

 and continuity theorems, weak convergence, and characterisitc functions.

 * HOL-Data_Structures: new and growing session of standard data

 structures.

 *** ML ***

 * The following combinators for low-level profiling of the ML runtime

 system are available:

   profile_time          (*CPU time*)

   profile_time_thread   (*CPU time on this thread*)

   profile_allocations   (*overall heap allocations*)

 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).

 * Antiquotation @{method NAME} inlines the (checked) name of the given

 Isar proof method.

 * Pretty printing of Poly/ML compiler output in Isabelle has been

 improved: proper treatment of break offsets and blocks with consistent

 breaks.

 * The auxiliary module Pure/display.ML has been eliminated. Its

 elementary thm print operations are now in Pure/more_thm.ML and thus

 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.

 * Simproc programming interfaces have been simplified:

 Simplifier.make_simproc and Simplifier.define_simproc supersede various

 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that

 term patterns for the left-hand sides are specified with implicitly

 fixed variables, like top-level theorem statements. INCOMPATIBILITY.

 * Instantiation rules have been re-organized as follows:

   Thm.instantiate  (*low-level instantiation with named arguments*)

   Thm.instantiate' (*version with positional arguments*)

   Drule.infer_instantiate  (*instantiation with type inference*)

   Drule.infer_instantiate'  (*version with positional arguments*)

 The LHS only requires variable specifications, instead of full terms.

 Old cterm_instantiate is superseded by infer_instantiate.

 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.

 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been

 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.

 instead (with proper context).

 * Thm.instantiate (and derivatives) no longer require the LHS of the

 instantiation to be certified: plain variables are given directly.

 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous

 quasi-bound variables (like the Simplifier), instead of accidentally

 named local fixes. This has the potential to improve stability of proof

 tools, but can also cause INCOMPATIBILITY for tools that don't observe

 the proof context discipline.

 * Isar proof methods are based on a slightly more general type

 context_tactic, which allows to change the proof context dynamically

 (e.g. to update cases) and indicate explicit Seq.Error results. Former

 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are

 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.

 *** System ***

 * Command-line tool "isabelle console" enables print mode "ASCII".

 * Command-line tool "isabelle update_then" expands old Isar command

 conflations:

     hence  ~>  then have

     thus   ~>  then show

 This syntax is more orthogonal and improves readability and

 maintainability of proofs.

 * Global session timeout is multiplied by timeout_scale factor. This

 allows to adjust large-scale tests (e.g. AFP) to overall hardware

 performance.

 * Property values in etc/symbols may contain spaces, if written with the

 replacement character "␣" (Unicode point 0x2324). For example:

     \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono

 * Java runtime environment for x86_64-windows allows to use larger heap

 space.

 * Java runtime options are determined separately for 32bit vs. 64bit

 platforms as follows.

   - Isabelle desktop application: platform-specific files that are

     associated with the main app bundle

   - isabelle jedit: settings

     JEDIT_JAVA_SYSTEM_OPTIONS

     JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

   - isabelle build: settings

     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

 * Bash shell function "jvmpath" has been renamed to "platform_path": it

 is relevant both for Poly/ML and JVM processes.

 * Poly/ML default platform architecture may be changed from 32bit to

 64bit via system option ML_system_64. A system restart (and rebuild) is

 required after change.

 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which

 both allow larger heap space than former x86-cygwin.

 * Heap images are 10-15% smaller due to less wasteful persistent theory

 content (using ML type theory_id instead of theory);

 New in Isabelle2015 (May 2015)

 ------------------------------

 *** General ***

 * Local theory specification commands may have a 'private' or

 'qualified' modifier to restrict name space accesses to the local scope,

 as provided by some "context begin ... end" block. For example:

   context

   begin

   private definition ...

   private lemma ...

   qualified definition ...

   qualified lemma ...

   lemma ...

   theorem ...

   end

 * Command 'experiment' opens an anonymous locale context with private

 naming policy.

 * Command 'notepad' requires proper nesting of begin/end and its proof

 structure in the body: 'oops' is no longer supported here. Minor

 INCOMPATIBILITY, use 'sorry' instead.

 * Command 'named_theorems' declares a dynamic fact within the context,

 together with an attribute to maintain the content incrementally. This

 supersedes functor Named_Thms in Isabelle/ML, but with a subtle change

 of semantics due to external visual order vs. internal reverse order.

 * 'find_theorems': search patterns which are abstractions are

 schematically expanded before search. Search results match the naive

 expectation more closely, particularly wrt. abbreviations.

 INCOMPATIBILITY.

 * Commands 'method_setup' and 'attribute_setup' now work within a local

 theory context.

 * Outer syntax commands are managed authentically within the theory

 context, without implicit global state. Potential for accidental

 INCOMPATIBILITY, make sure that required theories are really imported.

 * Historical command-line terminator ";" is no longer accepted (and

 already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle

 update_semicolons" to remove obsolete semicolons from old theory

 sources.

 * Structural composition of proof methods (meth1; meth2) in Isar

 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

 * The Eisbach proof method language allows to define new proof methods

 by combining existing ones with their usual syntax. The "match" proof

 method provides basic fact/term matching in addition to

 premise/conclusion matching through Subgoal.focus, and binds fact names

 from matches as well as term patterns within matches. The Isabelle

 documentation provides an entry "eisbach" for the Eisbach User Manual.

 Sources and various examples are in ~~/src/HOL/Eisbach/.

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

 * Improved folding mode "isabelle" based on Isar syntax. Alternatively,

 the "sidekick" mode may be used for document structure.

 * Extended bracket matching based on Isar language structure. System

 option jedit_structure_limit determines maximum number of lines to scan

 in the buffer.

 * Support for BibTeX files: context menu, context-sensitive token

 marker, SideKick parser.

 * Document antiquotation @{cite} provides formal markup, which is

 interpreted semi-formally based on .bib files that happen to be open in

 the editor (hyperlinks, completion etc.).

 * Less waste of vertical space via negative line spacing (see Global

 Options / Text Area).

 * Improved graphview panel with optional output of PNG or PDF, for

 display of 'thy_deps', 'class_deps' etc.

 * The commands 'thy_deps' and 'class_deps' allow optional bounds to

 restrict the visualized hierarchy.

 * Improved scheduling for asynchronous print commands (e.g. provers

 managed by the Sledgehammer panel) wrt. ongoing document processing.

 *** Document preparation ***

 * Document markup commands 'chapter', 'section', 'subsection',

 'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any

 context, even before the initial 'theory' command. Obsolete proof

 commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been

 discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'

 instead. The old 'header' command is still retained for some time, but

 should be replaced by 'chapter', 'section' etc. (using "isabelle

 update_header"). Minor INCOMPATIBILITY.

 * Official support for "tt" style variants, via \isatt{...} or

 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or

 verbatim environment of LaTeX is no longer used. This allows @{ML} etc.

 as argument to other macros (such as footnotes).

 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"

 style.

 * Discontinued obsolete option "document_graph": session_graph.pdf is

 produced unconditionally for HTML browser_info and PDF-LaTeX document.

 * Diagnostic commands and document markup commands within a proof do not

 affect the command tag for output. Thus commands like 'thm' are subject

 to proof document structure, and no longer "stick out" accidentally.

 Commands 'text' and 'txt' merely differ in the LaTeX style, not their

 tags. Potential INCOMPATIBILITY in exotic situations.

 * System option "pretty_margin" is superseded by "thy_output_margin",

 which is also accessible via document antiquotation option "margin".

 Only the margin for document output may be changed, but not the global

 pretty printing: that is 76 for plain console output, and adapted

 dynamically in GUI front-ends. Implementations of document

 antiquotations need to observe the margin explicitly according to

 Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

 * Specification of 'document_files' in the session ROOT file is

 mandatory for document preparation. The legacy mode with implicit

 copying of the document/ directory is no longer supported. Minor

 INCOMPATIBILITY.

 *** Pure ***

 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"

 etc.) allow an optional context of local variables ('for' declaration):

 these variables become schematic in the instantiated theorem; this

 behaviour is analogous to 'for' in attributes "where" and "of".

 Configuration option rule_insts_schematic (default false) controls use

 of schematic variables outside the context. Minor INCOMPATIBILITY,

 declare rule_insts_schematic = true temporarily and update to use local

 variable declarations or dummy patterns instead.

 * Explicit instantiation via attributes "where", "of", and proof methods

 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns

 ("_") that stand for anonymous local variables.

 * Generated schematic variables in standard format of exported facts are

 incremented to avoid material in the proof context. Rare

 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

 different index.

 * Lexical separation of signed and unsigned numerals: categories "num"

 and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence

 of numeral signs, particularly in expressions involving infix syntax

 like "(- 1) ^ n".

 * Old inner token category "xnum" has been discontinued.  Potential

 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"

 token category instead.

 *** HOL ***

 * New (co)datatype package:

   - The 'datatype_new' command has been renamed 'datatype'. The old

     command of that name is now called 'old_datatype' and is provided

     by "~~/src/HOL/Library/Old_Datatype.thy". See

     'isabelle doc datatypes' for information on porting.

     INCOMPATIBILITY.

   - Renamed theorems:

       disc_corec ~> corec_disc

       disc_corec_iff ~> corec_disc_iff

       disc_exclude ~> distinct_disc

       disc_exhaust ~> exhaust_disc

       disc_map_iff ~> map_disc_iff

       sel_corec ~> corec_sel

       sel_exhaust ~> exhaust_sel

       sel_map ~> map_sel

       sel_set ~> set_sel

       sel_split ~> split_sel

       sel_split_asm ~> split_sel_asm

       strong_coinduct ~> coinduct_strong

       weak_case_cong ~> case_cong_weak

     INCOMPATIBILITY.

   - The "no_code" option to "free_constructors", "datatype_new", and

     "codatatype" has been renamed "plugins del: code".

     INCOMPATIBILITY.

   - The rules "set_empty" have been removed. They are easy

     consequences of other set rules "by auto".

     INCOMPATIBILITY.

   - The rule "set_cases" is now registered with the "[cases set]"

     attribute. This can influence the behavior of the "cases" proof

     method when more than one case rule is applicable (e.g., an

     assumption is of the form "w : set ws" and the method "cases w"

     is invoked). The solution is to specify the case rule explicitly

     (e.g. "cases w rule: widget.exhaust").

     INCOMPATIBILITY.

   - Renamed theories:

       BNF_Comp ~> BNF_Composition

       BNF_FP_Base ~> BNF_Fixpoint_Base

       BNF_GFP ~> BNF_Greatest_Fixpoint

       BNF_LFP ~> BNF_Least_Fixpoint

       BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions

       Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions

     INCOMPATIBILITY.

   - Lifting and Transfer setup for basic HOL types sum and prod (also

     option) is now performed by the BNF package. Theories Lifting_Sum,

     Lifting_Product and Lifting_Option from Main became obsolete and

     were removed. Changed definitions of the relators rel_prod and

     rel_sum (using inductive).

     INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead

     of rel_prod_def and rel_sum_def.

     Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names

     changed (e.g. map_prod_transfer ~> prod.map_transfer).

   - Parametricity theorems for map functions, relators, set functions,

     constructors, case combinators, discriminators, selectors and

     (co)recursors are automatically proved and registered as transfer

     rules.

 * Old datatype package:

   - The old 'datatype' command has been renamed 'old_datatype', and

     'rep_datatype' has been renamed 'old_rep_datatype'. They are

     provided by "~~/src/HOL/Library/Old_Datatype.thy". See

     'isabelle doc datatypes' for information on porting.

     INCOMPATIBILITY.

   - Renamed theorems:

       weak_case_cong ~> case_cong_weak

     INCOMPATIBILITY.

   - Renamed theory:

       ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy

     INCOMPATIBILITY.

 * Nitpick:

   - Fixed soundness bug related to the strict and non-strict subset

     operations.

 * Sledgehammer:

   - CVC4 is now included with Isabelle instead of CVC3 and run by

     default.

   - Z3 is now always enabled by default, now that it is fully open

     source. The "z3_non_commercial" option is discontinued.

   - Minimization is now always enabled by default.

     Removed sub-command:

       min

   - Proof reconstruction, both one-liners and Isar, has been

     dramatically improved.

   - Improved support for CVC4 and veriT.

 * Old and new SMT modules:

   - The old 'smt' method has been renamed 'old_smt' and moved to

     'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,

     until applications have been ported to use the new 'smt' method. For

     the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must

     be installed, and the environment variable "OLD_Z3_SOLVER" must

     point to it.

     INCOMPATIBILITY.

   - The 'smt2' method has been renamed 'smt'.

     INCOMPATIBILITY.

   - New option 'smt_reconstruction_step_timeout' to limit the

     reconstruction time of Z3 proof steps in the new 'smt' method.

   - New option 'smt_statistics' to display statistics of the new 'smt'

     method, especially runtime statistics of Z3 proof reconstruction.

 * Lifting: command 'lift_definition' allows to execute lifted constants

 that have as a return type a datatype containing a subtype. This

 overcomes long-time limitations in the area of code generation and

 lifting, and avoids tedious workarounds.

 * Command and antiquotation "value" provide different evaluation slots

 (again), where the previous strategy (NBE after ML) serves as default.

 Minor INCOMPATIBILITY.

 * Add NO_MATCH-simproc, allows to check for syntactic non-equality.

 * field_simps: Use NO_MATCH-simproc for distribution rules, to avoid

 non-termination in case of distributing a division. With this change

 field_simps is in some cases slightly less powerful, if it fails try to

 add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.

 * Separate class no_zero_divisors has been given up in favour of fully

 algebraic semiring_no_zero_divisors. INCOMPATIBILITY.

 * Class linordered_semidom really requires no zero divisors.

 INCOMPATIBILITY.

 * Classes division_ring, field and linordered_field always demand

 "inverse 0 = 0". Given up separate classes division_ring_inverse_zero,

 field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.

 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit

 additive inverse operation. INCOMPATIBILITY.

 * Complex powers and square roots. The functions "ln" and "powr" are now

 overloaded for types real and complex, and 0 powr y = 0 by definition.

 INCOMPATIBILITY: type constraints may be necessary.

 * The functions "sin" and "cos" are now defined for any type of sort

 "{real_normed_algebra_1,banach}" type, so in particular on "real" and

 "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be

 needed.

 * New library of properties of the complex transcendental functions sin,

 cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.

 * The factorial function, "fact", now has type "nat => 'a" (of a sort

 that admits numeric types including nat, int, real and complex.

 INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type

 constraint, and the combination "real (fact k)" is likely to be

 unsatisfactory. If a type conversion is still necessary, then use

 "of_nat (fact k)" or "real_of_nat (fact k)".

 * Removed functions "natfloor" and "natceiling", use "nat o floor" and

 "nat o ceiling" instead. A few of the lemmas have been retained and

 adapted: in their names "natfloor"/"natceiling" has been replaced by

 "nat_floor"/"nat_ceiling".

 * Qualified some duplicated fact names required for boostrapping the

 type class hierarchy:

   ab_add_uminus_conv_diff ~> diff_conv_add_uminus

   field_inverse_zero ~> inverse_zero

   field_divide_inverse ~> divide_inverse

   field_inverse ~> left_inverse

 Minor INCOMPATIBILITY.

 * Eliminated fact duplicates:

   mult_less_imp_less_right ~> mult_right_less_imp_less

   mult_less_imp_less_left ~> mult_left_less_imp_less

 Minor INCOMPATIBILITY.

 * Fact consolidation: even_less_0_iff is subsumed by

 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).

 * Generalized and consolidated some theorems concerning divsibility:

   dvd_reduce ~> dvd_add_triv_right_iff

   dvd_plus_eq_right ~> dvd_add_right_iff

   dvd_plus_eq_left ~> dvd_add_left_iff

 Minor INCOMPATIBILITY.

 * "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"

 and part of theory Main.

   even_def ~> even_iff_mod_2_eq_zero

 INCOMPATIBILITY.

 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor

 INCOMPATIBILITY.

 * Bootstrap of listsum as special case of abstract product over lists.

 Fact rename:

     listsum_def ~> listsum.eq_foldr

 INCOMPATIBILITY.

 * Product over lists via constant "listprod".

 * Theory List: renamed drop_Suc_conv_tl and nth_drop' to

 Cons_nth_drop_Suc.

 * New infrastructure for compiling, running, evaluating and testing

 generated code in target languages in HOL/Library/Code_Test. See

 HOL/Codegenerator_Test/Code_Test* for examples.

 * Library/Multiset:

   - Introduced "replicate_mset" operation.

   - Introduced alternative characterizations of the multiset ordering in

     "Library/Multiset_Order".

   - Renamed multiset ordering:

       <# ~> #<#

       <=# ~> #<=#

       \<subset># ~> #\<subset>#

       \<subseteq># ~> #\<subseteq>#

     INCOMPATIBILITY.

   - Introduced abbreviations for ill-named multiset operations:

       <#, \<subset># abbreviate < (strict subset)

       <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)

     INCOMPATIBILITY.

   - Renamed

       in_multiset_of ~> in_multiset_in_set

       Multiset.fold ~> fold_mset

       Multiset.filter ~> filter_mset

     INCOMPATIBILITY.

   - Removed mcard, is equal to size.

   - Added attributes:

       image_mset.id [simp]

       image_mset_id [simp]

       elem_multiset_of_set [simp, intro]

       comp_fun_commute_plus_mset [simp]

       comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]

       in_mset_fold_plus_iff [iff]

       set_of_Union_mset [simp]

       in_Union_mset_iff [iff]

     INCOMPATIBILITY.