NEWS

moved method "use" to Pure;
more documentation;

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

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


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

*** General ***

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

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

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

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

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

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

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

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


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

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

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

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

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure.

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

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

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

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


*** Isar ***

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

* 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 old proof method "default" has been removed (legacy since
Isabelle2016). INCOMPATIBILITY, use "standard" instead.

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


*** Pure ***

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


*** HOL ***

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

* Theory Library/LaTeXsugar.thy: 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.

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

* Theory Library/Combinator_PER.thy: combinator to build partial
equivalence relations from a predicate and an equivalence relation.

* Theory Library/Perm.thy: basic facts about almost everywhere fix
bijections.

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

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

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

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

* Conventional syntax "%(). t" for unit abstractions.  Slight syntactic
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.

* Probability/Random_Permutations.thy contains some theory about 
choosing a permutation of a set uniformly at random and folding over a 
list in random order.

* Probability/SPMF formalises discrete subprobability distributions.

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

* Library/Set_Permutations.thy (executably) defines the set of 
permutations of a set, i.e. the set of all lists that contain every 
element of the carrier set exactly once.

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

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

* Sledgehammer:
  - 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 => bool) => 'a F => 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.

* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
linorder_cases instead.

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

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

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

* 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
    le_empty ~> subset_eq_empty
    mset_less_add_bothsides ~> mset_subset_add_bothsides
    mset_less_empty_nonempty ~> mset_subset_empty_nonempty
    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

* Multisets are now ordered with the multiset ordering
    #\<subseteq># ~> \<le>
    #\<subset># ~> <
    le_multiset ~> less_eq_multiset
    less_multiset ~> le_multiset
INCOMPATIBILITY.

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

* 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
    less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
    less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
INCOMPATIBILITY.

* 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,
and linordered_cancel_ab_semigroup_add.
INCOMPATIBILITY.

* There are some new simplification rules about multisets and the multiset
ordering.
INCOMPATIBILITY.

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

* More complex analysis including Cauchy's inequality, Liouville theorem,
open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma.

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

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

* Added topological_monoid

* Library/Complete_Partial_Order2.thy provides reasoning support for
proofs about monotonicity and continuity in chain-complete partial
orders and about admissibility conditions for fixpoint inductions.

* Library/Polynomial.thy contains also derivation of polynomials
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.

* Library/Sublist.thy: added function "prefixes" and renamed
  prefixeq -> prefix
  prefix -> strict_prefix
  suffixeq -> suffix
  suffix -> strict_suffix
  Added theory of longest common prefixes.

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

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

* In HOL-Probability the type of emeasure and nn_integral was changed
from ereal to ennreal:
  emeasure :: 'a measure => 'a set => ennreal
  nn_integral :: 'a measure => ('a => ennreal) => ennreal
INCOMPATIBILITY.


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

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

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

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

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

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

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

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

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

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



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