NEWS

more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

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

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

*** General ***

* Command 'experiment' opens an anonymous locale context with private
naming policy.

* Structural composition of proof methods (meth1; meth2) in Isar
corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

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

* Commands 'method_setup' and 'attribute_setup' now work within a local
theory context.

* Command 'named_theorems' declares a dynamic fact within the context,
together with an attribute to maintain the content incrementally. This
supersedes functor Named_Thms, but with a subtle change of semantics due
to external visual order vs. internal reverse order.

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

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

* 'find_theorems': search patterns which are abstractions are
schematically expanded before search. Search results match the naive
expectation more closely, particularly wrt. abbreviations.
INCOMPATIBILITY.


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

* Old graph browser (Java/AWT 1.0) is superseded by improved graphview
panel, which also includes PDF output.

* 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 opened
in the editor (hyperlinks, completion etc.).

* Less waste of vertical space via negative line spacing (see Global
Options / Text Area).


*** Pure ***

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

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

* Command "class_deps" takes optional sort arguments constraining
the search space.

* Lexical separation of signed and unsigend numerals: categories "num"
and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
of numeral signs, particulary 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 ***

* Given up separate type class no_zero_divisors 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.

* Type classes cancel_ab_semigroup_add / cancel_monoid_add specify
explicit additive inverse operation.  INCOMPATIBILITY.

* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
  single-step rewriting with subterm selection based on patterns.

* The functions "sin" and "cos" are now defined for any "'{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).

* Discontinued old-fashioned "codegen" tool. Code generation can always
be externally triggered using an appropriate ROOT file plus a
corresponding theory. Parametrization is possible using environment
variables, or ML snippets in the most extreme cases. Minor
INCOMPATIBILITY.

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

* 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 HOL-Main.
  even_def ~> even_iff_mod_2_eq_zero
INCOMPATIBILITY.

* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
Minor INCOMPATIBILITY.

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

* Bootstrap of listsum as special case of abstract product over lists.
Fact rename:
    listsum_def ~> listsum.eq_foldr
INCOMPATIBILITY.

* Command and antiquotation "value" provide different evaluation slots
(again), where the previous strategy (nbe after ML) serves as default.
Minor INCOMPATIBILITY.

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

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

* Product over lists via constant "listprod".

* Nitpick:
  - Fixed soundness bug related to the strict and nonstrict subset
    operations.

* Sledgehammer:
  - CVC4 is now included with Isabelle instead of CVC3 and run by
    default.
  - Minimization is now always enabled by default.
    Removed subcommand:
      min
  - The 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.

* 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/Sum_of_Squares: simplified and improved "sos" method. Always
use local CSDP executable, which is much faster than the NEOS server.
The "sos_cert" functionality is invoked as "sos" with additional
argument. Minor INCOMPATIBILITY.

* Theory "Library/Multiset":
  - Introduced "replicate_mset" operation.
  - Introduced alternative characterizations of the multiset ordering in
    "Library/Multiset_Order".
  - Renamed
      in_multiset_of ~> in_multiset_in_set
    INCOMPATIBILITY.
  - 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.

* HOL-Decision_Procs:
  - New counterexample generator quickcheck[approximation] for
    inequalities of transcendental functions.
    Uses hardware floating point arithmetic to randomly discover
    potential counterexamples. Counterexamples are certified with the
    'approximation' method.
    See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
    examples.

* HOL-Probability: Reworked measurability prover
  - applies destructor rules repeatetly
  - removed application splitting (replaced by destructor rule)
  - added congruence rules to rewrite measure spaces under the sets
    projection


*** Document preparation ***

* Discontinued obsolete option "document_graph": session_graph.pdf is
produced unconditionally for HTML browser_info and PDF-LaTeX document.

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

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

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


*** ML ***

* Subtle change of name space policy: undeclared entries are now
considered inaccessible, instead of accessible via the fully-qualified
internal name. This mainly affects Name_Space.intern (and derivatives),
which may produce an unexpected Long_Name.hidden prefix. Note that
contempory applications use the strict Name_Space.check (and
derivatives) instead, which is not affected by the change. Potential
INCOMPATIBILITY in rare applications of Name_Space.intern.

* The main operations to certify logical entities are Thm.ctyp_of and
Thm.cterm_of with a local context; old-style global theory variants are
available as Thm.global_ctyp_of and Thm.global_cterm_of.
INCOMPATIBILITY.

* Elementary operations in module Thm are no longer pervasive.
INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
Thm.term_of etc.

* Former combinators NAMED_CRITICAL and CRITICAL for central critical
sections have been discontinued, in favour of the more elementary
Multithreading.synchronized and its high-level derivative
Synchronized.var (which is usually sufficient in applications). Subtle
INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
nested.

* Cartouches within ML sources are turned into values of type
Input.source (with formal position information).

* Proper context for various elementary tactics: assume_tac,
resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.

* Tactical PARALLEL_ALLGOALS is the most common way to refer to
PARALLEL_GOALS.

* Basic combinators map, fold, fold_map, split_list, apply are
available as parameterized antiquotations, e.g. @{map 4} for lists of
quadruples.

* Renamed "pairself" to "apply2", in accordance to @{apply 2}.
INCOMPATIBILITY.

* Synchronized.value (ML) is actually synchronized (as in Scala):
subtle change of semantics with minimal potential for INCOMPATIBILITY.

* Goal.prove_multi is superseded by the fully general Goal.prove_common,
which also allows to specify a fork priority.


*** System ***

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY.

* JVM system property "isabelle.threads" determines size of Scala thread
pool, like Isabelle system option "threads" for ML.

* JVM system property "isabelle.laf" determines the default Swing
look-and-feel, via internal class name or symbolic name as in the jEdit
menu Global Options / Appearance.

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

* Historical command-line terminator ";" is no longer accepted.  Minor
INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
semicolons from theory sources.

* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.

* The Isabelle tool "build" provides new options -k and -x.



New in Isabelle2014 (August 2014)
---------------------------------

*** General ***

* Support for official Standard ML within the Isabelle context.
Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
and 'SML_export' allow to exchange toplevel bindings between the two
separate environments.  See also ~~/src/Tools/SML/Examples.thy for
some examples.

* Standard tactics and proof methods such as "clarsimp", "auto" and
"safe" now preserve equality hypotheses "x = expr" where x is a free
variable.  Locale assumptions and chained facts containing "x"
continue to be useful.  The new method "hypsubst_thin" and the
configuration option "hypsubst_thin" (within the attribute name space)
restore the previous behavior.  INCOMPATIBILITY, especially where
induction is done after these methods or when the names of free and
bound variables clash.  As first approximation, old proofs may be
repaired by "using [[hypsubst_thin = true]]" in the critical spot.

* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax.  Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state.  In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception.  Potential INCOMPATIBILITY for non-conformant tactical
proof tools.

* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
supports input via ` (backquote).

* The outer syntax categories "text" (for formal comments and document
markup commands) and "altstring" (for literal fact references) allow
cartouches as well, in addition to the traditional mix of quotations.

* Syntax of document antiquotation @{rail} now uses \<newline> instead
of "\\", to avoid the optical illusion of escaped backslash within
string token.  General renovation of its syntax using text cartouches.
Minor INCOMPATIBILITY.

* Discontinued legacy_isub_isup, which was a temporary workaround for
Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts
old identifier syntax with \<^isub> or \<^isup>.  Potential
INCOMPATIBILITY.

* Document antiquotation @{url} produces markup for the given URL,
which results in an active hyperlink within the text.

* Document antiquotation @{file_unchecked} is like @{file}, but does
not check existence within the file-system.

* Updated and extended manuals: codegen, datatypes, implementation,
isar-ref, jedit, system.


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

* Improved Document panel: simplified interaction where every single
mouse click (re)opens document via desktop environment or as jEdit
buffer.

* Support for Navigator plugin (with toolbar buttons), with connection
to PIDE hyperlinks.

* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.

* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.

* Improved syntactic and semantic completion mechanism, with simple
templates, completion language context, name-space completion,
file-name completion, spell-checker completion.

* Refined GUI popup for completion: more robust key/mouse event
handling and propagation to enclosing text area -- avoid loosing
keystrokes with slow / remote graphics displays.

* Completion popup supports both ENTER and TAB (default) to select an
item, depending on Isabelle options.

* Refined insertion of completion items wrt. jEdit text: multiple
selections, rectangular selections, rectangular selection as "tall
caret".

* Integrated spell-checker for document text, comments etc. with
completion popup and context-menu.

* More general "Query" panel supersedes "Find" panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context.  Minor incompatibility in keyboard
shortcuts etc.: replace action isabelle-find by isabelle-query.

* Search field for all output panels ("Output", "Query", "Info" etc.)
to highlight text via regular expression.

* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
General") allows to specify additional print modes for the prover
process, without requiring old-fashioned command-line invocation of
"isabelle jedit -m MODE".

* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.

* Empty editors buffers that are no longer required (e.g.\ via theory
imports) are automatically removed from the document model.

* Improved monitor panel.

* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.

* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
"Detach" a copy where this makes sense.

* New Simplifier Trace panel provides an interactive view of the
simplification process, enabled by the "simp_trace_new" attribute
within the context.


*** Pure ***

* Low-level type-class commands 'classes', 'classrel', 'arities' have
been discontinued to avoid the danger of non-trivial axiomatization
that is not immediately visible.  INCOMPATIBILITY, use regular
'instance' command with proof.  The required OFCLASS(...) theorem
might be postulated via 'axiomatization' beforehand, or the proof
finished trivially if the underlying class definition is made vacuous
(without any assumptions).  See also Isabelle/ML operations
Axclass.class_axiomatization, Axclass.classrel_axiomatization,
Axclass.arity_axiomatization.

* Basic constants of Pure use more conventional names and are always
qualified.  Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML.  The following
renaming needs to be applied:

  ==             ~>  Pure.eq
  ==>            ~>  Pure.imp
  all            ~>  Pure.all
  TYPE           ~>  Pure.type
  dummy_pattern  ~>  Pure.dummy_pattern

Systematic porting works by using the following theory setup on a
*previous* Isabelle version to introduce the new name accesses for the
old constants:

setup {*
  fn thy => thy
    |> Sign.root_path
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
    |> Sign.restore_naming thy
*}

Thus ML antiquotations like @{const_name Pure.eq} may be used already.
Later the application is moved to the current Isabelle version, and
the auxiliary aliases are deleted.

* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
instantiated theorem.

* Obsolete attribute "standard" has been discontinued (legacy since
Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
where instantiations with schematic variables are intended (for
declaration commands like 'lemmas' or attributes like "of").  The
following temporary definition may help to port old applications:

  attribute_setup standard =
    "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"

* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps).  Potential INCOMPATIBILITY, tools need to observe standard
context discipline.  See also Assumption.add_assumes and the more
primitive Thm.assume_hyps.

* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently, e.g. via cartouches).

* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
but the latter is retained some time as Proof General legacy.

* Code generator preprocessor: explicit control of simp tracing on a
per-constant basis.  See attribute "code_preproc".


*** HOL ***

* Code generator: enforce case of identifiers only for strict target
language requirements.  INCOMPATIBILITY.

* Code generator: explicit proof contexts in many ML interfaces.
INCOMPATIBILITY.

* Code generator: minimize exported identifiers by default.  Minor
INCOMPATIBILITY.

* Code generation for SML and OCaml: dropped arcane "no_signatures"
option.  Minor INCOMPATIBILITY.

* "declare [[code abort: ...]]" replaces "code_abort ...".
INCOMPATIBILITY.

* "declare [[code drop: ...]]" drops all code equations associated
with the given constants.

* Code generations are provided for make, fields, extend and truncate
operations on records.

* Command and antiquotation "value" are now hardcoded against nbe and
ML.  Minor INCOMPATIBILITY.

* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.

* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

* Qualified String.implode and String.explode.  INCOMPATIBILITY.

* Simplifier: Enhanced solver of preconditions of rewrite rules can
now deal with conjunctions.  For help with converting proofs, the old
behaviour of the simplifier can be restored like this: declare/using
[[simp_legacy_precond]].  This configuration option will disappear
again in the future.  INCOMPATIBILITY.

* Simproc "finite_Collect" is no longer enabled by default, due to
spurious crashes and other surprises.  Potential INCOMPATIBILITY.

* Moved new (co)datatype package and its dependencies from session
  "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',
  'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
  part of theory "Main".

  Theory renamings:
    FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
    Library/Wfrec.thy ~> Wfrec.thy
    Library/Zorn.thy ~> Zorn.thy
    Cardinals/Order_Relation.thy ~> Order_Relation.thy
    Library/Order_Union.thy ~> Cardinals/Order_Union.thy
    Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
    Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
    Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
    Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
    Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
    BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
    BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
    BNF/BNF_Comp.thy ~> BNF_Comp.thy
    BNF/BNF_Def.thy ~> BNF_Def.thy
    BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
    BNF/BNF_GFP.thy ~> BNF_GFP.thy
    BNF/BNF_LFP.thy ~> BNF_LFP.thy
    BNF/BNF_Util.thy ~> BNF_Util.thy
    BNF/Coinduction.thy ~> Coinduction.thy
    BNF/More_BNFs.thy ~> Library/More_BNFs.thy
    BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
    BNF/Examples/* ~> BNF_Examples/*

  New theories:
    Wellorder_Extension.thy (split from Zorn.thy)
    Library/Cardinal_Notations.thy
    Library/BNF_Axomatization.thy
    BNF_Examples/Misc_Primcorec.thy
    BNF_Examples/Stream_Processor.thy

  Discontinued theories:
    BNF/BNF.thy
    BNF/Equiv_Relations_More.thy

INCOMPATIBILITY.

* New (co)datatype package:
  - Command 'primcorec' is fully implemented.
  - Command 'datatype_new' generates size functions ("size_xxx" and
    "size") as required by 'fun'.
  - BNFs are integrated with the Lifting tool and new-style
    (co)datatypes with Transfer.
  - Renamed commands:
      datatype_new_compat ~> datatype_compat
      primrec_new ~> primrec
      wrap_free_constructors ~> free_constructors
    INCOMPATIBILITY.
  - The generated constants "xxx_case" and "xxx_rec" have been renamed
    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
    INCOMPATIBILITY.
  - The constant "xxx_(un)fold" and related theorems are no longer
    generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually
    using "prim(co)rec".
    INCOMPATIBILITY.
  - No discriminators are generated for nullary constructors by
    default, eliminating the need for the odd "=:" syntax.
    INCOMPATIBILITY.
  - No discriminators or selectors are generated by default by
    "datatype_new", unless custom names are specified or the new
    "discs_sels" option is passed.
    INCOMPATIBILITY.

* Old datatype package:
  - The generated theorems "xxx.cases" and "xxx.recs" have been
    renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
    "sum.case").  INCOMPATIBILITY.
  - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
    been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
    "prod_case" ~> "case_prod").  INCOMPATIBILITY.

* The types "'a list" and "'a option", their set and map functions,
  their relators, and their selectors are now produced using the new
  BNF-based datatype package.

  Renamed constants:
    Option.set ~> set_option
    Option.map ~> map_option
    option_rel ~> rel_option

  Renamed theorems:
    set_def ~> set_rec[abs_def]
    map_def ~> map_rec[abs_def]
    Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    option.recs ~> option.rec
    list_all2_def ~> list_all2_iff
    set.simps ~> set_simps (or the slightly different "list.set")
    map.simps ~> list.map
    hd.simps ~> list.sel(1)
    tl.simps ~> list.sel(2-3)
    the.simps ~> option.sel

INCOMPATIBILITY.

* The following map functions and relators have been renamed:
    sum_map ~> map_sum
    map_pair ~> map_prod
    prod_rel ~> rel_prod
    sum_rel ~> rel_sum
    fun_rel ~> rel_fun
    set_rel ~> rel_set
    filter_rel ~> rel_filter
    fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
    cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
    vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")

INCOMPATIBILITY.

* Lifting and Transfer:
  - a type variable as a raw type is supported
  - stronger reflexivity prover
  - rep_eq is always generated by lift_definition
  - setup for Lifting/Transfer is now automated for BNFs
    + holds for BNFs that do not contain a dead variable
    + relator_eq, relator_mono, relator_distr, relator_domain,
      relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
      right_unique, right_total, left_unique, left_total are proved
      automatically
    + definition of a predicator is generated automatically
    + simplification rules for a predicator definition are proved
      automatically for datatypes
  - consolidation of the setup of Lifting/Transfer
    + property that a relator preservers reflexivity is not needed any
      more
      Minor INCOMPATIBILITY.
    + left_total and left_unique rules are now transfer rules
      (reflexivity_rule attribute not needed anymore)
      INCOMPATIBILITY.
    + Domainp does not have to be a separate assumption in
      relator_domain theorems (=> more natural statement)
      INCOMPATIBILITY.
  - registration of code equations is more robust
    Potential INCOMPATIBILITY.
  - respectfulness proof obligation is preprocessed to a more readable
    form
    Potential INCOMPATIBILITY.
  - eq_onp is always unfolded in respectfulness proof obligation
    Potential INCOMPATIBILITY.
  - unregister lifting setup for Code_Numeral.integer and
    Code_Numeral.natural
    Potential INCOMPATIBILITY.
  - Lifting.invariant -> eq_onp
    INCOMPATIBILITY.

* New internal SAT solver "cdclite" that produces models and proof
traces.  This solver replaces the internal SAT solvers "enumerate" and
"dpll".  Applications that explicitly used one of these two SAT
solvers should use "cdclite" instead. In addition, "cdclite" is now
the default SAT solver for the "sat" and "satx" proof methods and
corresponding tactics; the old default can be restored using "declare
[[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.

* SMT module: A new version of the SMT module, temporarily called
"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
supported as oracles. Yices is no longer supported, because no version
of the solver can handle both SMT-LIB 2 and quantifiers.

* Activation of Z3 now works via "z3_non_commercial" system option
(without requiring restart), instead of former settings variable
"Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.

* Sledgehammer:
  - Z3 can now produce Isar proofs.
  - MaSh overhaul:
    . New SML-based learning algorithms eliminate the dependency on
      Python and increase performance and reliability.
    . MaSh and MeSh are now used by default together with the
      traditional MePo (Meng-Paulson) relevance filter. To disable
      MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
      Options / Isabelle / General to "none".
  - New option:
      smt_proofs
  - Renamed options:
      isar_compress ~> compress
      isar_try0 ~> try0

INCOMPATIBILITY.

* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.

* Nitpick:
  - Fixed soundness bug whereby mutually recursive datatypes could
    take infinite values.
  - Fixed soundness bug with low-level number functions such as
    "Abs_Integ" and "Rep_Integ".
  - Removed "std" option.
  - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
    "hide_types".

* Metis: Removed legacy proof method 'metisFT'. Use 'metis
(full_types)' instead. INCOMPATIBILITY.

* Try0: Added 'algebra' and 'meson' to the set of proof methods.

* Adjustion of INF and SUP operations:
  - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
  - Consolidated theorem names containing INFI and SUPR: have INF and
    SUP instead uniformly.
  - More aggressive normalization of expressions involving INF and Inf
    or SUP and Sup.
  - INF_image and SUP_image do not unfold composition.
  - Dropped facts INF_comp, SUP_comp.
  - Default congruence rules strong_INF_cong and strong_SUP_cong, with
    simplifier implication in premises.  Generalize and replace former
    INT_cong, SUP_cong

INCOMPATIBILITY.

* SUP and INF generalized to conditionally_complete_lattice.

* Swapped orientation of facts image_comp and vimage_comp:

  image_compose ~> image_comp [symmetric]
  image_comp ~> image_comp [symmetric]
  vimage_compose ~> vimage_comp [symmetric]
  vimage_comp ~> vimage_comp [symmetric]

INCOMPATIBILITY.

* Theory reorganization: split of Big_Operators.thy into
Groups_Big.thy and Lattices_Big.thy.

* Consolidated some facts about big group operators:

    setsum_0' ~> setsum.neutral
    setsum_0 ~> setsum.neutral_const
    setsum_addf ~> setsum.distrib
    setsum_cartesian_product ~> setsum.cartesian_product
    setsum_cases ~> setsum.If_cases
    setsum_commute ~> setsum.commute
    setsum_cong ~> setsum.cong
    setsum_delta ~> setsum.delta
    setsum_delta' ~> setsum.delta'
    setsum_diff1' ~> setsum.remove
    setsum_empty ~> setsum.empty
    setsum_infinite ~> setsum.infinite
    setsum_insert ~> setsum.insert
    setsum_inter_restrict'' ~> setsum.inter_filter
    setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
    setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
    setsum_mono_zero_left ~> setsum.mono_neutral_left
    setsum_mono_zero_right ~> setsum.mono_neutral_right
    setsum_reindex ~> setsum.reindex
    setsum_reindex_cong ~> setsum.reindex_cong
    setsum_reindex_nonzero ~> setsum.reindex_nontrivial
    setsum_restrict_set ~> setsum.inter_restrict
    setsum_Plus ~> setsum.Plus
    setsum_setsum_restrict ~> setsum.commute_restrict
    setsum_Sigma ~> setsum.Sigma
    setsum_subset_diff ~> setsum.subset_diff
    setsum_Un_disjoint ~> setsum.union_disjoint
    setsum_UN_disjoint ~> setsum.UNION_disjoint
    setsum_Un_Int ~> setsum.union_inter
    setsum_Union_disjoint ~> setsum.Union_disjoint
    setsum_UNION_zero ~> setsum.Union_comp
    setsum_Un_zero ~> setsum.union_inter_neutral
    strong_setprod_cong ~> setprod.strong_cong
    strong_setsum_cong ~> setsum.strong_cong
    setprod_1' ~> setprod.neutral
    setprod_1 ~> setprod.neutral_const
    setprod_cartesian_product ~> setprod.cartesian_product
    setprod_cong ~> setprod.cong
    setprod_delta ~> setprod.delta
    setprod_delta' ~> setprod.delta'
    setprod_empty ~> setprod.empty
    setprod_infinite ~> setprod.infinite
    setprod_insert ~> setprod.insert
    setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
    setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
    setprod_mono_one_left ~> setprod.mono_neutral_left
    setprod_mono_one_right ~> setprod.mono_neutral_right
    setprod_reindex ~> setprod.reindex
    setprod_reindex_cong ~> setprod.reindex_cong
    setprod_reindex_nonzero ~> setprod.reindex_nontrivial
    setprod_Sigma ~> setprod.Sigma
    setprod_subset_diff ~> setprod.subset_diff
    setprod_timesf ~> setprod.distrib
    setprod_Un2 ~> setprod.union_diff2
    setprod_Un_disjoint ~> setprod.union_disjoint
    setprod_UN_disjoint ~> setprod.UNION_disjoint
    setprod_Un_Int ~> setprod.union_inter
    setprod_Union_disjoint ~> setprod.Union_disjoint
    setprod_Un_one ~> setprod.union_inter_neutral

  Dropped setsum_cong2 (simple variant of setsum.cong).
  Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
  Dropped setsum_reindex_id, setprod_reindex_id
    (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).

INCOMPATIBILITY.

* Abolished slightly odd global lattice interpretation for min/max.

  Fact consolidations:
    min_max.inf_assoc ~> min.assoc
    min_max.inf_commute ~> min.commute
    min_max.inf_left_commute ~> min.left_commute
    min_max.inf_idem ~> min.idem
    min_max.inf_left_idem ~> min.left_idem
    min_max.inf_right_idem ~> min.right_idem
    min_max.sup_assoc ~> max.assoc
    min_max.sup_commute ~> max.commute
    min_max.sup_left_commute ~> max.left_commute
    min_max.sup_idem ~> max.idem
    min_max.sup_left_idem ~> max.left_idem
    min_max.sup_inf_distrib1 ~> max_min_distrib2
    min_max.sup_inf_distrib2 ~> max_min_distrib1
    min_max.inf_sup_distrib1 ~> min_max_distrib2
    min_max.inf_sup_distrib2 ~> min_max_distrib1
    min_max.distrib ~> min_max_distribs
    min_max.inf_absorb1 ~> min.absorb1
    min_max.inf_absorb2 ~> min.absorb2
    min_max.sup_absorb1 ~> max.absorb1
    min_max.sup_absorb2 ~> max.absorb2
    min_max.le_iff_inf ~> min.absorb_iff1
    min_max.le_iff_sup ~> max.absorb_iff2
    min_max.inf_le1 ~> min.cobounded1
    min_max.inf_le2 ~> min.cobounded2
    le_maxI1, min_max.sup_ge1 ~> max.cobounded1
    le_maxI2, min_max.sup_ge2 ~> max.cobounded2
    min_max.le_infI1 ~> min.coboundedI1
    min_max.le_infI2 ~> min.coboundedI2
    min_max.le_supI1 ~> max.coboundedI1
    min_max.le_supI2 ~> max.coboundedI2
    min_max.less_infI1 ~> min.strict_coboundedI1
    min_max.less_infI2 ~> min.strict_coboundedI2
    min_max.less_supI1 ~> max.strict_coboundedI1
    min_max.less_supI2 ~> max.strict_coboundedI2
    min_max.inf_mono ~> min.mono
    min_max.sup_mono ~> max.mono
    min_max.le_infI, min_max.inf_greatest ~> min.boundedI
    min_max.le_supI, min_max.sup_least ~> max.boundedI
    min_max.le_inf_iff ~> min.bounded_iff
    min_max.le_sup_iff ~> max.bounded_iff

For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
min.left_commute, min.left_idem, max.commute, max.assoc,
max.left_commute, max.left_idem directly.

For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
min.cobounded2, max.cobounded1m max.cobounded2 directly.

For min_ac or max_ac, prefer more general collection ac_simps.

INCOMPATIBILITY.

* Theorem disambiguation Inf_le_Sup (on finite sets) ~>
Inf_fin_le_Sup_fin.  INCOMPATIBILITY.

* Qualified constant names Wellfounded.acc, Wellfounded.accp.
INCOMPATIBILITY.

* Fact generalization and consolidation:
    neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1

INCOMPATIBILITY.

* Purely algebraic definition of even.  Fact generalization and
  consolidation:
    nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
    even_zero_(nat|int) ~> even_zero

INCOMPATIBILITY.

* Abolished neg_numeral.
  - Canonical representation for minus one is "- 1".
  - Canonical representation for other negative numbers is "- (numeral _)".
  - When devising rule sets for number calculation, consider the
    following canonical cases: 0, 1, numeral _, - 1, - numeral _.
  - HOLogic.dest_number also recognizes numerals in non-canonical forms
    like "numeral One", "- numeral One", "- 0" and even "- ... - _".
  - Syntax for negative numerals is mere input syntax.

INCOMPATIBILITY.

* Reduced name variants for rules on associativity and commutativity:

    add_assoc ~> add.assoc
    add_commute ~> add.commute
    add_left_commute ~> add.left_commute
    mult_assoc ~> mult.assoc
    mult_commute ~> mult.commute
    mult_left_commute ~> mult.left_commute
    nat_add_assoc ~> add.assoc
    nat_add_commute ~> add.commute
    nat_add_left_commute ~> add.left_commute
    nat_mult_assoc ~> mult.assoc
    nat_mult_commute ~> mult.commute
    eq_assoc ~> iff_assoc
    eq_left_commute ~> iff_left_commute

INCOMPATIBILITY.

* Fact collections add_ac and mult_ac are considered old-fashioned.
Prefer ac_simps instead, or specify rules
(add|mult).(assoc|commute|left_commute) individually.

* Elimination of fact duplicates:
    equals_zero_I ~> minus_unique
    diff_eq_0_iff_eq ~> right_minus_eq
    nat_infinite ~> infinite_UNIV_nat
    int_infinite ~> infinite_UNIV_int

INCOMPATIBILITY.

* Fact name consolidation:
    diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
    minus_le_self_iff ~> neg_less_eq_nonneg
    le_minus_self_iff ~> less_eq_neg_nonpos
    neg_less_nonneg ~> neg_less_pos
    less_minus_self_iff ~> less_neg_neg [simp]

INCOMPATIBILITY.

* More simplification rules on unary and binary minus:
add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
minus_add_cancel, uminus_add_conv_diff.  These correspondingly have
been taken away from fact collections algebra_simps and field_simps.
INCOMPATIBILITY.

To restore proofs, the following patterns are helpful:

a) Arbitrary failing proof not involving "diff_def":
Consider simplification with algebra_simps or field_simps.

b) Lifting rules from addition to subtraction:
Try with "using <rule for addition> of [... "- _" ...]" by simp".

c) Simplification with "diff_def": just drop "diff_def".
Consider simplification with algebra_simps or field_simps;
or the brute way with
"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".

* Introduce bdd_above and bdd_below in theory
Conditionally_Complete_Lattices, use them instead of explicitly
stating boundedness of sets.

* ccpo.admissible quantifies only over non-empty chains to allow more
syntax-directed proof rules; the case of the empty chain shows up as
additional case in fixpoint induction proofs.  INCOMPATIBILITY.

* Removed and renamed theorems in Series:
  summable_le         ~>  suminf_le
  suminf_le           ~>  suminf_le_const
  series_pos_le       ~>  setsum_le_suminf
  series_pos_less     ~>  setsum_less_suminf
  suminf_ge_zero      ~>  suminf_nonneg
  suminf_gt_zero      ~>  suminf_pos
  suminf_gt_zero_iff  ~>  suminf_pos_iff
  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  suminf_0_le         ~>  suminf_nonneg [rotate]
  pos_summable        ~>  summableI_nonneg_bounded
  ratio_test          ~>  summable_ratio_test

  removed series_zero, replaced by sums_finite

  removed auxiliary lemmas:

    sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
    half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
    real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
    sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
    summable_convergent_sumr_iff, sumr_diff_mult_const

INCOMPATIBILITY.

* Replace (F)DERIV syntax by has_derivative:
  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"

  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"

  - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax

  - removed constant isDiff

  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
    input syntax.

  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.

  - Renamed FDERIV_... lemmas to has_derivative_...

  - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV

  - removed DERIV_intros, has_derivative_eq_intros

  - introduced derivative_intros and deriative_eq_intros which
    includes now rules for DERIV, has_derivative and
    has_vector_derivative.

  - Other renamings:
    differentiable_def        ~>  real_differentiable_def
    differentiableE           ~>  real_differentiableE
    fderiv_def                ~>  has_derivative_at
    field_fderiv_def          ~>  field_has_derivative_at
    isDiff_der                ~>  differentiable_def
    deriv_fderiv              ~>  has_field_derivative_def
    deriv_def                 ~>  DERIV_def

INCOMPATIBILITY.

* Include more theorems in continuous_intros. Remove the
continuous_on_intros, isCont_intros collections, these facts are now
in continuous_intros.

* Theorems about complex numbers are now stated only using Re and Im,
the Complex constructor is not used anymore. It is possible to use
primcorec to defined the behaviour of a complex-valued function.

Removed theorems about the Complex constructor from the simpset, they
are available as the lemma collection legacy_Complex_simps. This
especially removes

    i_complex_of_real: "ii * complex_of_real r = Complex 0 r".

Instead the reverse direction is supported with
    Complex_eq: "Complex a b = a + \<i> * b"

Moved csqrt from Fundamental_Algebra_Theorem to Complex.

  Renamings:
    Re/Im                  ~>  complex.sel
    complex_Re/Im_zero     ~>  zero_complex.sel
    complex_Re/Im_add      ~>  plus_complex.sel
    complex_Re/Im_minus    ~>  uminus_complex.sel
    complex_Re/Im_diff     ~>  minus_complex.sel
    complex_Re/Im_one      ~>  one_complex.sel
    complex_Re/Im_mult     ~>  times_complex.sel
    complex_Re/Im_inverse  ~>  inverse_complex.sel
    complex_Re/Im_scaleR   ~>  scaleR_complex.sel
    complex_Re/Im_i        ~>  ii.sel
    complex_Re/Im_cnj      ~>  cnj.sel
    Re/Im_cis              ~>  cis.sel

    complex_divide_def   ~>  divide_complex_def
    complex_norm_def     ~>  norm_complex_def
    cmod_def             ~>  norm_complex_de

  Removed theorems:
    complex_zero_def
    complex_add_def
    complex_minus_def
    complex_diff_def
    complex_one_def
    complex_mult_def
    complex_inverse_def
    complex_scaleR_def

INCOMPATIBILITY.

* Theory Lubs moved HOL image to HOL-Library. It is replaced by
Conditionally_Complete_Lattices.  INCOMPATIBILITY.

* HOL-Library: new theory src/HOL/Library/Tree.thy.

* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
is subsumed by session Kleene_Algebra in AFP.

* HOL-Library / theory RBT: various constants and facts are hidden;
lifting setup is unregistered.  INCOMPATIBILITY.

* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.

* HOL-Word: bit representations prefer type bool over type bit.
INCOMPATIBILITY.

* HOL-Word:
  - Abandoned fact collection "word_arith_alts", which is a duplicate
    of "word_arith_wis".
  - Dropped first (duplicated) element in fact collections
    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
    "uint_word_arith_bintrs".

* HOL-Number_Theory:
  - consolidated the proofs of the binomial theorem
  - the function fib is again of type nat => nat and not overloaded
  - no more references to Old_Number_Theory in the HOL libraries
    (except the AFP)

INCOMPATIBILITY.

* HOL-Multivariate_Analysis:
  - Type class ordered_real_vector for ordered vector spaces.
  - New theory Complex_Basic_Analysis defining complex derivatives,
    holomorphic functions, etc., ported from HOL Light's canal.ml.
  - Changed order of ordered_euclidean_space to be compatible with
    pointwise ordering on products. Therefore instance of
    conditionally_complete_lattice and ordered_real_vector.
    INCOMPATIBILITY: use box instead of greaterThanLessThan or
    explicit set-comprehensions with eucl_less for other (half-)open
    intervals.
  - removed dependencies on type class ordered_euclidean_space with
    introduction of "cbox" on euclidean_space
    - renamed theorems:
        interval ~> box
        mem_interval ~> mem_box
        interval_eq_empty ~> box_eq_empty
        interval_ne_empty ~> box_ne_empty
        interval_sing(1) ~> cbox_sing
        interval_sing(2) ~> box_sing
        subset_interval_imp ~> subset_box_imp
        subset_interval ~> subset_box
        open_interval ~> open_box
        closed_interval ~> closed_cbox
        interior_closed_interval ~> interior_cbox
        bounded_closed_interval ~> bounded_cbox
        compact_interval ~> compact_cbox
        bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
        bounded_subset_closed_interval ~> bounded_subset_cbox
        mem_interval_componentwiseI ~> mem_box_componentwiseI
        convex_box ~> convex_prod
        rel_interior_real_interval ~> rel_interior_real_box
        convex_interval ~> convex_box
        convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
        frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
        content_closed_interval' ~> content_cbox'
        elementary_subset_interval ~> elementary_subset_box
        diameter_closed_interval ~> diameter_cbox
        frontier_closed_interval ~> frontier_cbox
        frontier_open_interval ~> frontier_box
        bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
        closure_open_interval ~> closure_box
        open_closed_interval_convex ~> open_cbox_convex
        open_interval_midpoint ~> box_midpoint
        content_image_affinity_interval ~> content_image_affinity_cbox
        is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
        bounded_interval ~> bounded_closed_interval + bounded_boxes

    - respective theorems for intervals over the reals:
        content_closed_interval + content_cbox
        has_integral + has_integral_real
        fine_division_exists + fine_division_exists_real
        has_integral_null + has_integral_null_real
        tagged_division_union_interval + tagged_division_union_interval_real
        has_integral_const + has_integral_const_real
        integral_const + integral_const_real
        has_integral_bound + has_integral_bound_real
        integrable_continuous + integrable_continuous_real
        integrable_subinterval + integrable_subinterval_real
        has_integral_reflect_lemma + has_integral_reflect_lemma_real
        integrable_reflect + integrable_reflect_real
        integral_reflect + integral_reflect_real
        image_affinity_interval + image_affinity_cbox
        image_smult_interval + image_smult_cbox
        integrable_const + integrable_const_ivl
        integrable_on_subinterval + integrable_on_subcbox

  - renamed theorems:
    derivative_linear         ~>  has_derivative_bounded_linear
    derivative_is_linear      ~>  has_derivative_linear
    bounded_linear_imp_linear ~>  bounded_linear.linear

* HOL-Probability:
  - Renamed positive_integral to nn_integral:

    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
      positive_integral_positive ~> nn_integral_nonneg

    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.

  - replaced the Lebesgue integral on real numbers by the more general
    Bochner integral for functions into a real-normed vector space.

    integral_zero               ~>  integral_zero / integrable_zero
    integral_minus              ~>  integral_minus / integrable_minus
    integral_add                ~>  integral_add / integrable_add
    integral_diff               ~>  integral_diff / integrable_diff
    integral_setsum             ~>  integral_setsum / integrable_setsum
    integral_multc              ~>  integral_mult_left / integrable_mult_left
    integral_cmult              ~>  integral_mult_right / integrable_mult_right
    integral_triangle_inequality~>  integral_norm_bound
    integrable_nonneg           ~>  integrableI_nonneg
    integral_positive           ~>  integral_nonneg_AE
    integrable_abs_iff          ~>  integrable_abs_cancel
    positive_integral_lim_INF   ~>  nn_integral_liminf
    lebesgue_real_affine        ~>  lborel_real_affine
    borel_integral_has_integral ~>  has_integral_lebesgue_integral
    integral_indicator          ~>
         integral_real_indicator / integrable_real_indicator
    positive_integral_fst       ~>  nn_integral_fst'
    positive_integral_fst_measurable ~> nn_integral_fst
    positive_integral_snd_measurable ~> nn_integral_snd

    integrable_fst_measurable   ~>
         integral_fst / integrable_fst / AE_integrable_fst

    integrable_snd_measurable   ~>
         integral_snd / integrable_snd / AE_integrable_snd

    integral_monotone_convergence  ~>
         integral_monotone_convergence / integrable_monotone_convergence

    integral_monotone_convergence_at_top  ~>
         integral_monotone_convergence_at_top /
         integrable_monotone_convergence_at_top

    has_integral_iff_positive_integral_lebesgue  ~>
         has_integral_iff_has_bochner_integral_lebesgue_nonneg

    lebesgue_integral_has_integral  ~>
         has_integral_integrable_lebesgue_nonneg

    positive_integral_lebesgue_has_integral  ~>
         integral_has_integral_lebesgue_nonneg /
         integrable_has_integral_lebesgue_nonneg

    lebesgue_integral_real_affine  ~>
         nn_integral_real_affine

    has_integral_iff_positive_integral_lborel  ~>
         integral_has_integral_nonneg / integrable_has_integral_nonneg

    The following theorems where removed:

    lebesgue_integral_nonneg
    lebesgue_integral_uminus
    lebesgue_integral_cmult
    lebesgue_integral_multc
    lebesgue_integral_cmult_nonneg
    integral_cmul_indicator
    integral_real

  - Formalized properties about exponentially, Erlang, and normal
    distributed random variables.

* HOL-Decision_Procs: Separate command 'approximate' for approximative
computation in src/HOL/Decision_Procs/Approximation.  Minor
INCOMPATIBILITY.


*** Scala ***

* The signature and semantics of Document.Snapshot.cumulate_markup /
select_markup have been clarified.  Markup is now traversed in the
order of reports given by the prover: later markup is usually more
specific and may override results accumulated so far.  The elements
guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.

* Substantial reworking of internal PIDE protocol communication
channels.  INCOMPATIBILITY.