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

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

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

Isabelle2015).

*** Isar ***

* Command '\<proof>' is an alias for 'sorry', with different

typesetting. E.g. to produce proof holes in examples and documentation.

*** HOL ***

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

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

  - The "size" plugin has been made compatible again with locales.

* Renamed split_if -> if_split and split_if_asm -> if_split_asm to

resemble the f.split naming convention, 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.

* 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, Schwarz Lemma.

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

* Added topological_monoid

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

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

*** ML ***

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

*** System ***

* The Isabelle system environment always ensures that the main

executables are found within the shell search $PATH: "isabelle" and

"isabelle_scala_script".

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

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: