NEWS

dropped various legacy fact bindings

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

*** Isar ***

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


*** HOL ***

* (Co)datatype package:
  - 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.

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

* Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.

* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
  lcm_left_commute_nat ~> lcm.left_commute
  lcm_left_commute_int ~> lcm.left_commute
  gcd_left_commute_nat ~> gcd.left_commute
  gcd_left_commute_int ~> gcd.left_commute
  gcd_greatest_iff_nat ~> gcd_greatest_iff
  gcd_greatest_iff_int ~> gcd_greatest_iff
  coprime_dvd_mult_nat ~> coprime_dvd_mult
  coprime_dvd_mult_int ~> coprime_dvd_mult
  zpower_numeral_even ~> power_numeral_even
  gcd_mult_cancel_nat ~> gcd_mult_cancel
  gcd_mult_cancel_int ~> gcd_mult_cancel
  div_gcd_coprime_nat ~> div_gcd_coprime
  div_gcd_coprime_int ~> div_gcd_coprime
  zpower_numeral_odd ~> power_numeral_odd
  zero_less_int_conv ~> of_nat_0_less_iff
  gcd_greatest_nat ~> gcd_greatest
  gcd_greatest_int ~> gcd_greatest
  coprime_mult_nat ~> coprime_mult
  coprime_mult_int ~> coprime_mult
  lcm_commute_nat ~> lcm.commute
  lcm_commute_int ~> lcm.commute
  int_less_0_conv ~> of_nat_less_0_iff
  gcd_commute_nat ~> gcd.commute
  gcd_commute_int ~> gcd.commute
  Gcd_insert_nat ~> Gcd_insert
  Gcd_insert_int ~> Gcd_insert
  of_int_int_eq ~> of_int_of_nat_eq
  lcm_least_nat ~> lcm_least
  lcm_least_int ~> lcm_least
  lcm_assoc_nat ~> lcm.assoc
  lcm_assoc_int ~> lcm.assoc
  int_le_0_conv ~> of_nat_le_0_iff
  int_eq_0_conv ~> of_nat_eq_0_iff
  Gcd_empty_nat ~> Gcd_empty
  Gcd_empty_int ~> Gcd_empty
  gcd_assoc_nat ~> gcd.assoc
  gcd_assoc_int ~> gcd.assoc
  zero_zle_int ~> of_nat_0_le_iff
  lcm_dvd2_nat ~> dvd_lcm2
  lcm_dvd2_int ~> dvd_lcm2
  lcm_dvd1_nat ~> dvd_lcm1
  lcm_dvd1_int ~> dvd_lcm1
  gcd_zero_nat ~> gcd_eq_0_iff
  gcd_zero_int ~> gcd_eq_0_iff
  gcd_dvd2_nat ~> gcd_dvd2
  gcd_dvd2_int ~> gcd_dvd2
  gcd_dvd1_nat ~> gcd_dvd1
  gcd_dvd1_int ~> gcd_dvd1
  int_numeral ~> of_nat_numeral
  lcm_ac_nat ~> ac_simps
  lcm_ac_int ~> ac_simps
  gcd_ac_nat ~> ac_simps
  gcd_ac_int ~> ac_simps
  abs_int_eq ~> abs_of_nat
  zless_int ~> of_nat_less_iff
  zdiff_int ~> of_nat_diff
  zadd_int ~> of_nat_add
  int_mult ~> of_nat_mult
  int_Suc ~> of_nat_Suc
  inj_int ~> inj_of_nat
  int_1 ~> of_nat_1
  int_0 ~> of_nat_0
  realpow_minus_mult ~> power_minus_mult
  realpow_Suc_le_self ~> power_Suc_le_self
INCOMPATIBILITY.


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.

* HOL-Decision_Procs: The "approximation" method works with "powr"
(exponentiation on real numbers) again.

* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
integrals (= complex path integrals), Cauchy's integral theorem, winding
numbers and Cauchy's integral formula, Liouville theorem, Fundamental
Theorem of Algebra. Ported from HOL Light.

* HOL-Multivariate_Analysis: topological concepts such as connected
components, homotopic paths and the inside or outside of a set.

* HOL-Multivariate_Analysis: radius of convergence of power series and
various summability tests; Harmonic numbers and the Euler–Mascheroni
constant; the Generalised Binomial Theorem; the complex and real
Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
properties.

* HOL-Probability: The central limit theorem based on Levy's uniqueness
and continuity theorems, weak convergence, and characterisitc functions.

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


*** ML ***

* The following combinators for low-level profiling of the ML runtime
system are available:

  profile_time          (*CPU time*)
  profile_time_thread   (*CPU time on this thread*)
  profile_allocations   (*overall heap allocations*)

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

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

* Pretty printing of Poly/ML compiler output in Isabelle has been
improved: proper treatment of break offsets and blocks with consistent
breaks.

* The auxiliary module Pure/display.ML has been eliminated. Its
elementary thm print operations are now in Pure/more_thm.ML and thus
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.

* Simproc programming interfaces have been simplified:
Simplifier.make_simproc and Simplifier.define_simproc supersede various
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
term patterns for the left-hand sides are specified with implicitly
fixed variables, like top-level theorem statements. INCOMPATIBILITY.

* Instantiation rules have been re-organized as follows:

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

  Drule.infer_instantiate  (*instantiation with type inference*)
  Drule.infer_instantiate'  (*version with positional arguments*)

The LHS only requires variable specifications, instead of full terms.
Old cterm_instantiate is superseded by infer_instantiate.
INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.

* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
instead (with proper context).

* Thm.instantiate (and derivatives) no longer require the LHS of the
instantiation to be certified: plain variables are given directly.

* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous
quasi-bound variables (like the Simplifier), instead of accidentally
named local fixes. This has the potential to improve stability of proof
tools, but can also cause INCOMPATIBILITY for tools that don't observe
the proof context discipline.

* Isar proof methods are based on a slightly more general type
context_tactic, which allows to change the proof context dynamically
(e.g. to update cases) and indicate explicit Seq.Error results. Former
METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.


*** System ***

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

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

    hence  ~>  then have
    thus   ~>  then show

This syntax is more orthogonal and improves readability and
maintainability of proofs.

* Global session timeout is multiplied by timeout_scale factor. This
allows to adjust large-scale tests (e.g. AFP) to overall hardware
performance.

* Property values in etc/symbols may contain spaces, if written with the
replacement character "␣" (Unicode point 0x2324). For example:

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

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

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

  - Isabelle desktop application: platform-specific files that are
    associated with the main app bundle

  - isabelle jedit: settings
    JEDIT_JAVA_SYSTEM_OPTIONS
    JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

  - isabelle build: settings
    ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

* Bash shell function "jvmpath" has been renamed to "platform_path": it
is relevant both for Poly/ML and JVM processes.

* Poly/ML default platform architecture may be changed from 32bit to
64bit via system option ML_system_64. A system restart (and rebuild) is
required after change.

* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
both allow larger heap space than former x86-cygwin.

* Heap images are 10-15% smaller due to less wasteful persistent theory
content (using ML type theory_id instead of theory);



New in Isabelle2015 (May 2015)
------------------------------

*** General ***

* Local theory specification commands may have a 'private' or
'qualified' modifier to restrict name space accesses to the local scope,
as provided by some "context begin ... end" block. For example:

  context
  begin

  private definition ...
  private lemma ...

  qualified definition ...
  qualified lemma ...

  lemma ...
  theorem ...

  end

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

* Command 'notepad' requires proper nesting of begin/end and its proof
structure in the body: 'oops' is no longer supported here. Minor
INCOMPATIBILITY, use 'sorry' instead.

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

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

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

* Outer syntax commands are managed authentically within the theory
context, without implicit global state. Potential for accidental
INCOMPATIBILITY, make sure that required theories are really imported.

* Historical command-line terminator ";" is no longer accepted (and
already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
update_semicolons" to remove obsolete semicolons from old theory
sources.

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

* The Eisbach proof method language allows to define new proof methods
by combining existing ones with their usual syntax. The "match" proof
method provides basic fact/term matching in addition to
premise/conclusion matching through Subgoal.focus, and binds fact names
from matches as well as term patterns within matches. The Isabelle
documentation provides an entry "eisbach" for the Eisbach User Manual.
Sources and various examples are in ~~/src/HOL/Eisbach/.


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

* Improved folding mode "isabelle" based on Isar syntax. Alternatively,
the "sidekick" mode may be used for document structure.

* Extended bracket matching based on Isar language structure. System
option jedit_structure_limit determines maximum number of lines to scan
in the buffer.

* Support for BibTeX files: context menu, context-sensitive token
marker, SideKick parser.

* Document antiquotation @{cite} provides formal markup, which is
interpreted semi-formally based on .bib files that happen to be open in
the editor (hyperlinks, completion etc.).

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

* Improved graphview panel with optional output of PNG or PDF, for
display of 'thy_deps', 'class_deps' etc.

* The commands 'thy_deps' and 'class_deps' allow optional bounds to
restrict the visualized hierarchy.

* Improved scheduling for asynchronous print commands (e.g. provers
managed by the Sledgehammer panel) wrt. ongoing document processing.


*** Document preparation ***

* Document markup commands 'chapter', 'section', 'subsection',
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
context, even before the initial 'theory' command. Obsolete proof
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
instead. The old 'header' command is still retained for some time, but
should be replaced by 'chapter', 'section' etc. (using "isabelle
update_header"). Minor INCOMPATIBILITY.

* Official support for "tt" style variants, via \isatt{...} or
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
as argument to other macros (such as footnotes).

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

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

* Diagnostic commands and document markup commands within a proof do not
affect the command tag for output. Thus commands like 'thm' are subject
to proof document structure, and no longer "stick out" accidentally.
Commands 'text' and 'txt' merely differ in the LaTeX style, not their
tags. Potential INCOMPATIBILITY in exotic situations.

* System option "pretty_margin" is superseded by "thy_output_margin",
which is also accessible via document antiquotation option "margin".
Only the margin for document output may be changed, but not the global
pretty printing: that is 76 for plain console output, and adapted
dynamically in GUI front-ends. Implementations of document
antiquotations need to observe the margin explicitly according to
Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

* Specification of 'document_files' in the session ROOT file is
mandatory for document preparation. The legacy mode with implicit
copying of the document/ directory is no longer supported. Minor
INCOMPATIBILITY.


*** Pure ***

* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
etc.) allow an optional context of local variables ('for' declaration):
these variables become schematic in the instantiated theorem; this
behaviour is analogous to 'for' in attributes "where" and "of".
Configuration option rule_insts_schematic (default false) controls use
of schematic variables outside the context. Minor INCOMPATIBILITY,
declare rule_insts_schematic = true temporarily and update to use local
variable declarations or dummy patterns instead.

* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.

* Generated schematic variables in standard format of exported facts are
incremented to avoid material in the proof context. Rare
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
different index.

* Lexical separation of signed and unsigned numerals: categories "num"
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
of numeral signs, particularly in expressions involving infix syntax
like "(- 1) ^ n".

* Old inner token category "xnum" has been discontinued.  Potential
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
token category instead.


*** HOL ***

* New (co)datatype package:
  - The 'datatype_new' command has been renamed 'datatype'. The old
    command of that name is now called 'old_datatype' and is provided
    by "~~/src/HOL/Library/Old_Datatype.thy". See
    'isabelle doc datatypes' for information on porting.
    INCOMPATIBILITY.
  - Renamed theorems:
      disc_corec ~> corec_disc
      disc_corec_iff ~> corec_disc_iff
      disc_exclude ~> distinct_disc
      disc_exhaust ~> exhaust_disc
      disc_map_iff ~> map_disc_iff
      sel_corec ~> corec_sel
      sel_exhaust ~> exhaust_sel
      sel_map ~> map_sel
      sel_set ~> set_sel
      sel_split ~> split_sel
      sel_split_asm ~> split_sel_asm
      strong_coinduct ~> coinduct_strong
      weak_case_cong ~> case_cong_weak
    INCOMPATIBILITY.
  - The "no_code" option to "free_constructors", "datatype_new", and
    "codatatype" has been renamed "plugins del: code".
    INCOMPATIBILITY.
  - The rules "set_empty" have been removed. They are easy
    consequences of other set rules "by auto".
    INCOMPATIBILITY.
  - The rule "set_cases" is now registered with the "[cases set]"
    attribute. This can influence the behavior of the "cases" proof
    method when more than one case rule is applicable (e.g., an
    assumption is of the form "w : set ws" and the method "cases w"
    is invoked). The solution is to specify the case rule explicitly
    (e.g. "cases w rule: widget.exhaust").
    INCOMPATIBILITY.
  - Renamed theories:
      BNF_Comp ~> BNF_Composition
      BNF_FP_Base ~> BNF_Fixpoint_Base
      BNF_GFP ~> BNF_Greatest_Fixpoint
      BNF_LFP ~> BNF_Least_Fixpoint
      BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
      Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
    INCOMPATIBILITY.
  - Lifting and Transfer setup for basic HOL types sum and prod (also
    option) is now performed by the BNF package. Theories Lifting_Sum,
    Lifting_Product and Lifting_Option from Main became obsolete and
    were removed. Changed definitions of the relators rel_prod and
    rel_sum (using inductive).
    INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
    of rel_prod_def and rel_sum_def.
    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
    changed (e.g. map_prod_transfer ~> prod.map_transfer).
  - Parametricity theorems for map functions, relators, set functions,
    constructors, case combinators, discriminators, selectors and
    (co)recursors are automatically proved and registered as transfer
    rules.

* Old datatype package:
  - The old 'datatype' command has been renamed 'old_datatype', and
    'rep_datatype' has been renamed 'old_rep_datatype'. They are
    provided by "~~/src/HOL/Library/Old_Datatype.thy". See
    'isabelle doc datatypes' for information on porting.
    INCOMPATIBILITY.
  - Renamed theorems:
      weak_case_cong ~> case_cong_weak
    INCOMPATIBILITY.
  - Renamed theory:
      ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
    INCOMPATIBILITY.

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

* Sledgehammer:
  - CVC4 is now included with Isabelle instead of CVC3 and run by
    default.
  - Z3 is now always enabled by default, now that it is fully open
    source. The "z3_non_commercial" option is discontinued.
  - Minimization is now always enabled by default.
    Removed sub-command:
      min
  - Proof reconstruction, both one-liners and Isar, has been
    dramatically improved.
  - Improved support for CVC4 and veriT.

* Old and new SMT modules:
  - The old 'smt' method has been renamed 'old_smt' and moved to
    'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,
    until applications have been ported to use the new 'smt' method. For
    the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must
    be installed, and the environment variable "OLD_Z3_SOLVER" must
    point to it.
    INCOMPATIBILITY.
  - The 'smt2' method has been renamed 'smt'.
    INCOMPATIBILITY.
  - New option 'smt_reconstruction_step_timeout' to limit the
    reconstruction time of Z3 proof steps in the new 'smt' method.
  - New option 'smt_statistics' to display statistics of the new 'smt'
    method, especially runtime statistics of Z3 proof reconstruction.

* Lifting: command 'lift_definition' allows to execute lifted constants
that have as a return type a datatype containing a subtype. This
overcomes long-time limitations in the area of code generation and
lifting, and avoids tedious workarounds.

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

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

* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
non-termination in case of distributing a division. With this change
field_simps is in some cases slightly less powerful, if it fails try to
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.

* Separate class no_zero_divisors has been given up in favour of fully
algebraic semiring_no_zero_divisors. INCOMPATIBILITY.

* Class linordered_semidom really requires no zero divisors.
INCOMPATIBILITY.

* Classes division_ring, field and linordered_field always demand
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.

* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
additive inverse operation. INCOMPATIBILITY.

* Complex powers and square roots. The functions "ln" and "powr" are now
overloaded for types real and complex, and 0 powr y = 0 by definition.
INCOMPATIBILITY: type constraints may be necessary.

* The functions "sin" and "cos" are now defined for any type of sort
"{real_normed_algebra_1,banach}" type, so in particular on "real" and
"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
needed.

* New library of properties of the complex transcendental functions sin,
cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.

* The factorial function, "fact", now has type "nat => 'a" (of a sort
that admits numeric types including nat, int, real and complex.
INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
constraint, and the combination "real (fact k)" is likely to be
unsatisfactory. If a type conversion is still necessary, then use
"of_nat (fact k)" or "real_of_nat (fact k)".

* Removed functions "natfloor" and "natceiling", use "nat o floor" and
"nat o ceiling" instead. A few of the lemmas have been retained and
adapted: in their names "natfloor"/"natceiling" has been replaced by
"nat_floor"/"nat_ceiling".

* Qualified some duplicated fact names required for boostrapping the
type class hierarchy:
  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
  field_inverse_zero ~> inverse_zero
  field_divide_inverse ~> divide_inverse
  field_inverse ~> left_inverse
Minor INCOMPATIBILITY.

* Eliminated fact duplicates:
  mult_less_imp_less_right ~> mult_right_less_imp_less
  mult_less_imp_less_left ~> mult_left_less_imp_less
Minor INCOMPATIBILITY.

* Fact consolidation: even_less_0_iff is subsumed by
double_add_less_zero_iff_single_add_less_zero (simp by default anyway).

* Generalized and consolidated some theorems concerning divsibility:
  dvd_reduce ~> dvd_add_triv_right_iff
  dvd_plus_eq_right ~> dvd_add_right_iff
  dvd_plus_eq_left ~> dvd_add_left_iff
Minor INCOMPATIBILITY.

* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
and part of theory Main.
  even_def ~> even_iff_mod_2_eq_zero
INCOMPATIBILITY.

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

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

* Product over lists via constant "listprod".

* Theory List: renamed drop_Suc_conv_tl and nth_drop' to
Cons_nth_drop_Suc.

* New infrastructure for compiling, running, evaluating and testing
generated code in target languages in HOL/Library/Code_Test. See
HOL/Codegenerator_Test/Code_Test* for examples.

* Library/Multiset:
  - Introduced "replicate_mset" operation.
  - Introduced alternative characterizations of the multiset ordering in
    "Library/Multiset_Order".
  - Renamed multiset ordering:
      <# ~> #<#
      <=# ~> #<=#
      \<subset># ~> #\<subset>#
      \<subseteq># ~> #\<subseteq>#
    INCOMPATIBILITY.
  - Introduced abbreviations for ill-named multiset operations:
      <#, \<subset># abbreviate < (strict subset)
      <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
    INCOMPATIBILITY.
  - Renamed
      in_multiset_of ~> in_multiset_in_set
      Multiset.fold ~> fold_mset
      Multiset.filter ~> filter_mset
    INCOMPATIBILITY.
  - Removed mcard, is equal to size.
  - Added attributes:
      image_mset.id [simp]
      image_mset_id [simp]
      elem_multiset_of_set [simp, intro]
      comp_fun_commute_plus_mset [simp]
      comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
      in_mset_fold_plus_iff [iff]
      set_of_Union_mset [simp]
      in_Union_mset_iff [iff]
    INCOMPATIBILITY.

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

* 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 repeatedly
  - removed application splitting (replaced by destructor rule)
  - added congruence rules to rewrite measure spaces under the sets
    projection

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


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

* Subtle change of error semantics of Toplevel.proof_of: regular user
ERROR instead of internal Toplevel.UNDEF.

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

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

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

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

* Proper context for various elementary tactics: assume_tac,
resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,