Isabelle NEWS -- history of user-relevant changes

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

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

New in this Isabelle version

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

*** General ***

* Embedded content (e.g. the inner syntax of types, terms, props) may be

delimited uniformly via cartouches. This works better than old-fashioned

quotes when sub-languages are nested.

* Type-inference improves sorts of newly introduced type variables for

the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).

Thus terms like "f x" or "\<And>x. P x" without any further syntactic context

produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare

INCOMPATIBILITY, need to provide explicit type constraints for Pure

types where this is really intended.

* Simplified outer syntax: uniform category "name" includes long

identifiers. Former "xname" / "nameref" / "name reference" has been

discontinued.

* Mixfix annotations support general block properties, with syntax

"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",

"unbreakable", "markup". The existing notation "(DIGITS" is equivalent

to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks

is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.

* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --

this allows special forms of document output.

* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control

symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its

derivatives.

* \<^raw:...> symbols are no longer supported.

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

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

Isabelle2015).

* Command 'bundle' provides a local theory target to define a bundle

from the body of specification commands (such as 'declare',

'declaration', 'notation', 'lemmas', 'lemma'). For example:

bundle foo

begin

  declare a [simp]

  declare b [intro]

end

* Command 'unbundle' is like 'include', but works within a local theory

context. Unlike "context includes ... begin", the effect of 'unbundle'

on the target context persists, until different declarations are given.

* Splitter in simp, auto and friends:

- The syntax "split add" has been discontinued, use plain "split".

- For situations with many conditional or case expressions,

there is an alternative splitting strategy that can be much faster.

It is selected by writing "split!" instead of "split". It applies

safe introduction and elimination rules after each split rule.

As a result the subgoal may be split into several subgoals.

* Proof method "blast" is more robust wrt. corner cases of Pure

statements without object-logic judgment.

* Pure provides basic versions of proof methods "simp" and "simp_all"

that only know about meta-equality (==). Potential INCOMPATIBILITY in

theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order

is relevant to avoid confusion of Pure.simp vs. HOL.simp.

* Commands 'prf' and 'full_prf' are somewhat more informative (again):

proof terms are reconstructed and cleaned from administrative thm

nodes.

* The command 'unfolding' and proof method "unfold" include a second

stage where given equations are passed through the attribute "abs_def"

before rewriting. This ensures that definitions are fully expanded,

regardless of the actual parameters that are provided. Rare

INCOMPATIBILITY in some corner cases: use proof method (simp only:)

instead, or declare [[unfold_abs_def = false]] in the proof context.

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

* Dockable window "Symbols" also provides access to 'abbrevs' from the

outer syntax of the current theory buffer. This provides clickable

syntax templates, including entries with empty abbrevs name (which are

inaccessible via keyboard completion).

* Cartouche abbreviations work both for " and ` to accomodate typical

situations where old ASCII notation may be updated.

* Isabelle/ML and Standard ML files are presented in Sidekick with the

tree structure of section headings: this special comment format is

described in "implementation" chapter 0, e.g. (*** section ***).

* IDE support for the Isabelle/Pure bootstrap process, with the

following independent stages:

  src/Pure/ROOT0.ML

  src/Pure/ROOT.ML

  src/Pure/Pure.thy

  src/Pure/ML_Bootstrap.thy

The ML ROOT files act like quasi-theories in the context of theory

ML_Bootstrap: this allows continuous checking of all loaded ML files.

The theory files are presented with a modified header to import Pure

from the running Isabelle instance. Results from changed versions of

each stage are *not* propagated to the next stage, and isolated from the

actual Isabelle/Pure that runs the IDE itself. The sequential

dependencies of the above files are only observed for batch build.

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

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'

are treated as delimiters for fold structure; 'begin' and 'end'

structure of theory specifications is treated as well.

* Sidekick parser "isabelle-context" shows nesting of context blocks

according to 'begin' and 'end' structure.

* Syntactic indentation according to Isabelle outer syntax. Action

"indent-lines" (shortcut C+i) indents the current line according to

command keywords and some command substructure. Action

"isabelle.newline" (shortcut ENTER) indents the old and the new line

according to command keywords only; see also option

"jedit_indent_newline".

* Semantic indentation for unstructured proof scripts ('apply' etc.) via

number of subgoals. This requires information of ongoing document

processing and may thus lag behind, when the user is editing too

quickly; see also option "jedit_script_indent" and

"jedit_script_indent_limit".

* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all

occurences of the formal entity at the caret position. This facilitates

systematic renaming.

* Action "isabelle.keymap-merge" asks the user to resolve pending

Isabelle keymap changes that are in conflict with the current jEdit

keymap; non-conflicting changes are always applied implicitly. This

action is automatically invoked on Isabelle/jEdit startup and thus

increases chances that users see new keyboard shortcuts when re-using

old keymaps.

* Document markup works across multiple Isar commands, e.g. the results

established at the end of a proof are properly identified in the theorem

statement.

* Command 'proof' provides information about proof outline with cases,

e.g. for proof methods "cases", "induct", "goal_cases".

* Completion templates for commands involving "begin ... end" blocks,

e.g. 'context', 'notepad'.

* Additional abbreviations for syntactic completion may be specified

within the theory header as 'abbrevs'. The theory syntax for 'keywords'

has been simplified accordingly: optional abbrevs need to go into the

new 'abbrevs' section.

* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and

$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor

INCOMPATIBILITY, use 'abbrevs' within theory header instead.

* ML and document antiquotations for file-systems paths are more uniform

and diverse:

  @{path NAME}   -- no file-system check

  @{file NAME}   -- check for plain file

  @{dir NAME}    -- check for directory

Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may

have to be changed.

*** Isar ***

* The defining position of a literal fact \<open>prop\<close> is maintained more

carefully, and made accessible as hyperlink in the Prover IDE.

* Commands 'finally' and 'ultimately' used to expose the result as

literal fact: this accidental behaviour has been discontinued. Rare

INCOMPATIBILITY, use more explicit means to refer to facts in Isar.

* Command 'axiomatization' has become more restrictive to correspond

better to internal axioms as singleton facts with mandatory name. Minor

INCOMPATIBILITY.

* Many specification elements support structured statements with 'if' /

'for' eigen-context, e.g. 'axiomatization', 'abbreviation',

'definition', 'inductive', 'function'.

* Toplevel theorem statements support eigen-context notation with 'if' /

'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the

traditional long statement form (in prefix). Local premises are called

"that" or "assms", respectively. Empty premises are *not* bound in the

context: INCOMPATIBILITY.

* Command 'define' introduces a local (non-polymorphic) definition, with

optional abstraction over local parameters. The syntax resembles

'definition' and 'obtain'. It fits better into the Isar language than

old 'def', which is now a legacy feature.

* Command 'obtain' supports structured statements with 'if' / 'for'

context.

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

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

* The old proof method "default" has been removed (legacy since

Isabelle2016). INCOMPATIBILITY, use "standard" instead.

* Proof methods may refer to the main facts via the dynamic fact

"method_facts". This is particularly useful for Eisbach method

definitions.

* Proof method "use" allows to modify the main facts of a given method

expression, e.g.

  (use facts in simp)

  (use facts in \<open>simp add: ...\<close>)

*** Pure ***

* Code generator: config option "code_timing" triggers measurements of

different phases of code generation. See src/HOL/ex/Code_Timing.thy for

examples.

* Code generator: implicits in Scala (stemming from type class instances)

are generated into companion object of corresponding type class, to resolve

some situations where ambiguities may occur.

*** HOL ***

* New proof method "argo" using the built-in Argo solver based on SMT technology.

The method can be used to prove goals of quantifier-free propositional logic,

goals based on a combination of quantifier-free propositional logic with equality,

and goals based on a combination of quantifier-free propositional logic with

linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for

examples.

* Type class "div" with operation "mod" renamed to type class "modulo" with

operation "modulo", analogously to type class "divide".  This eliminates the

need to qualify any of those names in the presence of infix "mod" syntax.

INCOMPATIBILITY.

* The unique existence quantifier no longer provides 'binder' syntax,

but uses syntax translations (as for bounded unique existence). Thus

iterated quantification \<exists>!x y. P x y with its slightly confusing

sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,

pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y

(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential

INCOMPATIBILITY in rare situations.

* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.

* Moved measure theory from HOL-Probability to HOL-Analysis. When importing

HOL-Analysis some theorems need additional name spaces prefixes due to name

clashes.

INCOMPATIBILITY.

* In HOL-Probability the type of emeasure and nn_integral was changed

from ereal to ennreal:

  emeasure :: 'a measure => 'a set => ennreal

  nn_integral :: 'a measure => ('a => ennreal) => ennreal

INCOMPATIBILITY.

* HOL-Analysis: more complex analysis including Cauchy's inequality, Liouville theorem,

open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma.

* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman

Minkowski theorem.

* HOL-Analysis: Numerous results ported from the HOL Light libraries: homeomorphisms,

continuous function extensions and other advanced topics in topology

* Number_Theory: algebraic foundation for primes: Generalisation of

predicate "prime" and introduction of predicates "prime_elem",

"irreducible", a "prime_factorization" function, and the "factorial_ring"

typeclass with instance proofs for nat, int, poly. Some theorems now have

different names, most notably "prime_def" is now "prime_nat_iff".

INCOMPATIBILITY.

* Probability: Code generation and QuickCheck for Probability Mass

Functions.

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

and products.

* Theory List.thy:

  listsum ~> sum_list

  listprod ~> prod_list

* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying

equations in functional programming style: variables present on the

left-hand but not on the righ-hand side are replaced by underscores.

* "surj" is a mere input abbreviation, to avoid hiding an equation in

term output.  Minor INCOMPATIBILITY.

* Theory Library/Combinator_PER.thy: combinator to build partial

equivalence relations from a predicate and an equivalence relation.

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

bijections.

* Theory Library/Normalized_Fraction.thy: allows viewing an element

of a field of fractions as a normalized fraction (i.e. a pair of

numerator and denominator such that the two are coprime and the

denominator is normalized w.r.t. unit factors)

* Locale bijection establishes convenient default simp rules

like "inv f (f a) = a" for total bijections.

* Former locale lifting_syntax is now a bundle, which is easier to

include in a local context or theorem statement, e.g. "context includes

lifting_syntax begin ... end". Minor INCOMPATIBILITY.

* Code generation for scala: ambiguous implicts in class diagrams

are spelt out explicitly.

* Abstract locales semigroup, abel_semigroup, semilattice,

semilattice_neutr, ordering, ordering_top, semilattice_order,

semilattice_neutr_order, comm_monoid_set, semilattice_set,

semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set

monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,

comm_monoid_fun use boldified syntax uniformly that does not clash

with corresponding global syntax.  INCOMPATIBILITY.

* Conventional syntax "%(). t" for unit abstractions.  Slight syntactic

INCOMPATIBILITY.

* Command 'code_reflect' accepts empty constructor lists for datatypes,

which renders those abstract effectively.

* Command 'export_code' checks given constants for abstraction violations:

a small guarantee that given constants specify a safe interface for the

generated code.

* Probability/Random_Permutations.thy contains some theory about

choosing a permutation of a set uniformly at random and folding over a

list in random order.

* Probability/SPMF formalises discrete subprobability distributions.

* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax"

allow to control optional syntax in local contexts; this supersedes

former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle

finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax".

* Library/Set_Permutations.thy (executably) defines the set of

permutations of a set, i.e. the set of all lists that contain every

element of the carrier set exactly once.

* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on

explicitly provided auxiliary definitions for required type class

dictionaries rather than half-working magic.  INCOMPATIBILITY, see

the tutorial on code generation for details.

* New abbreviations for negated existence (but not bounded existence):

  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)

  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)

* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"

has been removed for output. It is retained for input only, until it is

eliminated altogether.

* metis: The problem encoding has changed very slightly. This might

break existing proofs. INCOMPATIBILITY.

* Sledgehammer:

  - The MaSh relevance filter is now faster than before.

  - Produce syntactically correct Vampire 4.0 problem files.

* The 'coinductive' command produces a proper coinduction rule for

mutual coinductive predicates. This new rule replaces the old rule,

which exposed details of the internal fixpoint construction and was

hard to use. INCOMPATIBILITY.

* (Co)datatype package:

  - New commands for defining corecursive functions and reasoning about

    them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',

    'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof

    method. See 'isabelle doc corec'.

  - The predicator :: ('a => bool) => 'a F => bool is now a first-class

    citizen in bounded natural functors.

  - 'primrec' now allows nested calls through the predicator in addition

    to the map function.

  - 'bnf' automatically discharges reflexive proof obligations.

  - 'bnf' outputs a slightly modified proof obligation expressing rel in

       terms of map and set

       (not giving a specification for rel makes this one reflexive).

  - 'bnf' outputs a new proof obligation expressing pred in terms of set

       (not giving a specification for pred makes this one reflexive).

    INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.

  - Renamed lemmas:

      rel_prod_apply ~> rel_prod_inject

      pred_prod_apply ~> pred_prod_inject

    INCOMPATIBILITY.

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

  - The theorems about "rel" and "set" may have a slightly different (but

    equivalent) form.

    INCOMPATIBILITY.

* Some old / obsolete theorems have been renamed / removed, potential

INCOMPATIBILITY.

  nat_less_cases  --  removed, use linorder_cases instead

  inv_image_comp  --  removed, use image_inv_f_f instead

  image_surj_f_inv_f  ~>  image_f_inv_f

* Some theorems about groups and orders have been generalised from

  groups to semi-groups that are also monoids:

    le_add_same_cancel1

    le_add_same_cancel2

    less_add_same_cancel1

    less_add_same_cancel2

    add_le_same_cancel1

    add_le_same_cancel2

    add_less_same_cancel1

    add_less_same_cancel2

* Some simplifications theorems about rings have been removed, since

  superseeded by a more general version:

    less_add_cancel_left_greater_zero ~> less_add_same_cancel1

    less_add_cancel_right_greater_zero ~> less_add_same_cancel2

    less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1

    less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2

    less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1

    less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2

    less_add_cancel_left_less_zero ~> add_less_same_cancel1

    less_add_cancel_right_less_zero ~> add_less_same_cancel2

INCOMPATIBILITY.

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

resemble the f.split naming convention, INCOMPATIBILITY.

* Characters (type char) are modelled as finite algebraic type

corresponding to {0..255}.

  - Logical representation:

    * 0 is instantiated to the ASCII zero character.

    * All other characters are represented as "Char n"

      with n being a raw numeral expression less than 256.

    * Expressions of the form "Char n" with n greater than 255

      are non-canonical.

  - Printing and parsing:

    * Printable characters are printed and parsed as "CHR ''\<dots>''"

      (as before).

    * The ASCII zero character is printed and parsed as "0".

    * All other canonical characters are printed as "CHR 0xXX"

      with XX being the hexadecimal character code.  "CHR n"

      is parsable for every numeral expression n.

    * Non-canonical characters have no special syntax and are

      printed as their logical representation.

  - Explicit conversions from and to the natural numbers are

    provided as char_of_nat, nat_of_char (as before).

  - The auxiliary nibble type has been discontinued.

INCOMPATIBILITY.

* Multiset membership is now expressed using set_mset rather than count.

  - Expressions "count M a > 0" and similar simplify to membership

    by default.

  - Converting between "count M a = 0" and non-membership happens using

    equations count_eq_zero_iff and not_in_iff.

  - Rules count_inI and in_countE obtain facts of the form

    "count M a = n" from membership.

  - Rules count_in_diffI and in_diff_countE obtain facts of the form

    "count M a = n + count N a" from membership on difference sets.

INCOMPATIBILITY.

* The names of multiset theorems have been normalised to distinguish which

  ordering the theorems are about

    mset_less_eqI ~> mset_subset_eqI

    mset_less_insertD ~> mset_subset_insertD

    mset_less_eq_count ~> mset_subset_eq_count

    mset_less_diff_self ~> mset_subset_diff_self

    mset_le_exists_conv ~> mset_subset_eq_exists_conv

    mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel

    mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel

    mset_le_mono_add ~> mset_subset_eq_mono_add

    mset_le_add_left ~> mset_subset_eq_add_left

    mset_le_add_right ~> mset_subset_eq_add_right

    mset_le_single ~> mset_subset_eq_single

    mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute

    diff_le_self ~> diff_subset_eq_self

    mset_leD ~> mset_subset_eqD

    mset_lessD ~> mset_subsetD

    mset_le_insertD ~> mset_subset_eq_insertD

    mset_less_of_empty ~> mset_subset_of_empty

    le_empty ~> subset_eq_empty

    mset_less_add_bothsides ~> mset_subset_add_bothsides

    mset_less_empty_nonempty ~> mset_subset_empty_nonempty

    mset_less_size ~> mset_subset_size

    wf_less_mset_rel ~> wf_subset_mset_rel

    count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq

    mset_remdups_le ~> mset_remdups_subset_eq

    ms_lesseq_impl ~> subset_eq_mset_impl

  Some functions have been renamed:

    ms_lesseq_impl -> subset_eq_mset_impl

* Multisets are now ordered with the multiset ordering

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

    #\<subset># ~> <

    le_multiset ~> less_eq_multiset

    less_multiset ~> le_multiset

INCOMPATIBILITY.

* The prefix multiset_order has been discontinued: the theorems can be directly

accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset"

have been discontinued, and the interpretations "multiset_linorder" and

"multiset_wellorder" have been replaced by instantiations.

INCOMPATIBILITY.

* Some theorems about the multiset ordering have been renamed:

    le_multiset_def ~> less_eq_multiset_def

    less_multiset_def ~> le_multiset_def

    less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset

    mult_less_not_refl ~> mset_le_not_refl

    mult_less_trans ~> mset_le_trans

    mult_less_not_sym ~> mset_le_not_sym

    mult_less_asym ~> mset_le_asym

    mult_less_irrefl ~> mset_le_irrefl

    union_less_mono2{,1,2} ~> union_le_mono2{,1,2}

    le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O

    le_multiset_total ~> less_eq_multiset_total

    less_multiset_right_total ~> subset_eq_imp_le_multiset

    le_multiset_empty_left ~> less_eq_multiset_empty_left

    le_multiset_empty_right ~> less_eq_multiset_empty_right

    less_multiset_empty_right ~> le_multiset_empty_left

    less_multiset_empty_left ~> le_multiset_empty_right

    union_less_diff_plus ~> union_le_diff_plus

    ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset

    less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty

    le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty

    less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff

    less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff

INCOMPATIBILITY.

* The lemma mset_map has now the attribute [simp].

INCOMPATIBILITY.

* Some theorems about multisets have been removed:

    le_multiset_plus_plus_left_iff ~> add_less_cancel_right

    le_multiset_plus_plus_right_iff ~> add_less_cancel_left

    add_eq_self_empty_iff ~> add_cancel_left_right

    mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right

INCOMPATIBILITY.

* Some typeclass constraints about multisets have been reduced from ordered or

linordered to preorder. Multisets have the additional typeclasses order_bot,

no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,

linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.

INCOMPATIBILITY.

* There are some new simplification rules about multisets, the multiset

ordering, and the subset ordering on multisets.

INCOMPATIBILITY.

* The subset ordering on multisets has now the interpretations

ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot.

INCOMPATIBILITY.

* Multiset: single has been removed in favor of add_mset that roughly

corresponds to Set.insert. Some theorems have removed or changed:

  single_not_empty ~> add_mset_not_empty or empty_not_add_mset

  fold_mset_insert ~> fold_mset_add_mset

  image_mset_insert ~> image_mset_add_mset

  union_single_eq_diff

  multi_self_add_other_not_self

  diff_single_eq_union

INCOMPATIBILITY.

* Multiset: some theorems have been changed to use add_mset instead of single:

  mset_add

  multi_self_add_other_not_self

  diff_single_eq_union

  union_single_eq_diff

  union_single_eq_member

  add_eq_conv_diff

  insert_noteq_member

  add_eq_conv_ex

  multi_member_split

  multiset_add_sub_el_shuffle

  mset_subset_eq_insertD

  mset_subset_insertD

  insert_subset_eq_iff

  insert_union_subset_iff

  multi_psub_of_add_self

  inter_add_left1

  inter_add_left2

  inter_add_right1

  inter_add_right2

  sup_union_left1

  sup_union_left2

  sup_union_right1

  sup_union_right2

  size_eq_Suc_imp_eq_union

  multi_nonempty_split

  mset_insort

  mset_update

  mult1I

  less_add

  mset_zip_take_Cons_drop_twice

  rel_mset_Zero

  msed_map_invL

  msed_map_invR

  msed_rel_invL

  msed_rel_invR

  le_multiset_right_total

  multiset_induct

  multiset_induct2_size

  multiset_induct2

INCOMPATIBILITY.

* Multiset: the definitions of some constants have changed to use add_mset instead

of adding a single element:

  image_mset

  mset

  replicate_mset

  mult1

  pred_mset

  rel_mset'

  mset_insort

INCOMPATIBILITY.

* Due to the above changes, the attributes of some multiset theorems have

been changed:

  insert_DiffM  [] ~> [simp]

  insert_DiffM2 [simp] ~> []

  diff_add_mset_swap [simp]

  fold_mset_add_mset [simp]

  diff_diff_add [simp] (for multisets only)

  diff_cancel [simp] ~> []

  count_single [simp] ~> []

  set_mset_single [simp] ~> []

  size_multiset_single [simp] ~> []

  size_single [simp] ~> []

  image_mset_single [simp] ~> []

  mset_subset_eq_mono_add_right_cancel [simp] ~> []

  mset_subset_eq_mono_add_left_cancel [simp] ~> []

  fold_mset_single [simp] ~> []

  subset_eq_empty [simp] ~> []

  empty_sup [simp] ~> []

  sup_empty [simp] ~> []

  inter_empty [simp] ~> []

  empty_inter [simp] ~> []

INCOMPATIBILITY.

* The order of the variables in the second cases of multiset_induct,

multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A).

INCOMPATIBILITY.

* There is now a simplification procedure on multisets. It mimics the behavior

of the procedure on natural numbers.

INCOMPATIBILITY.

* Renamed sums and products of multisets:

  msetsum ~> sum_mset

  msetprod ~> prod_mset

* The symbols for intersection and union of multisets have been changed:

  #\<inter> ~> \<inter>#

  #\<union> ~> \<union>#

INCOMPATIBILITY.

* The lemma one_step_implies_mult_aux on multisets has been removed, use

one_step_implies_mult instead.

INCOMPATIBILITY.

* The following theorems have been renamed:

  setsum_left_distrib ~> setsum_distrib_right

  setsum_right_distrib ~> setsum_distrib_left

INCOMPATIBILITY.

* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.

INCOMPATIBILITY.

* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional

comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)".

* Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.

* The type class ordered_comm_monoid_add is now called

ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is

introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add.

INCOMPATIBILITY.

* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.

* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When

instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit

instantiation of ordered_ab_semigroup_monoid_add_imp_le might be

required.

INCOMPATIBILITY.

* Added topological_monoid

* Library/Complete_Partial_Order2.thy provides reasoning support for

proofs about monotonicity and continuity in chain-complete partial

orders and about admissibility conditions for fixpoint inductions.

* Library/Polynomial.thy contains also derivation of polynomials

but not gcd/lcm on polynomials over fields.  This has been moved

to a separate theory Library/Polynomial_GCD_euclidean.thy, to

pave way for a possible future different type class instantiation

for polynomials over factorial rings.  INCOMPATIBILITY.

* Library/Sublist.thy: added function "prefixes" and renamed

  prefixeq -> prefix

  prefix -> strict_prefix

  suffixeq -> suffix

  suffix -> strict_suffix

  Added theory of longest common prefixes.

* Dropped various legacy fact bindings, whose replacements are often

of a more general type also:

  lcm_left_commute_nat ~> lcm.left_commute

  lcm_left_commute_int ~> lcm.left_commute

  gcd_left_commute_nat ~> gcd.left_commute

  gcd_left_commute_int ~> gcd.left_commute

  gcd_greatest_iff_nat ~> gcd_greatest_iff

  gcd_greatest_iff_int ~> gcd_greatest_iff

  coprime_dvd_mult_nat ~> coprime_dvd_mult

  coprime_dvd_mult_int ~> coprime_dvd_mult

  zpower_numeral_even ~> power_numeral_even

  gcd_mult_cancel_nat ~> gcd_mult_cancel

  gcd_mult_cancel_int ~> gcd_mult_cancel

  div_gcd_coprime_nat ~> div_gcd_coprime

  div_gcd_coprime_int ~> div_gcd_coprime

  zpower_numeral_odd ~> power_numeral_odd

  zero_less_int_conv ~> of_nat_0_less_iff

  gcd_greatest_nat ~> gcd_greatest

  gcd_greatest_int ~> gcd_greatest

  coprime_mult_nat ~> coprime_mult

  coprime_mult_int ~> coprime_mult

  lcm_commute_nat ~> lcm.commute

  lcm_commute_int ~> lcm.commute

  int_less_0_conv ~> of_nat_less_0_iff

  gcd_commute_nat ~> gcd.commute

  gcd_commute_int ~> gcd.commute

  Gcd_insert_nat ~> Gcd_insert

  Gcd_insert_int ~> Gcd_insert

  of_int_int_eq ~> of_int_of_nat_eq

  lcm_least_nat ~> lcm_least

  lcm_least_int ~> lcm_least

  lcm_assoc_nat ~> lcm.assoc

  lcm_assoc_int ~> lcm.assoc

  int_le_0_conv ~> of_nat_le_0_iff

  int_eq_0_conv ~> of_nat_eq_0_iff

  Gcd_empty_nat ~> Gcd_empty

  Gcd_empty_int ~> Gcd_empty

  gcd_assoc_nat ~> gcd.assoc

  gcd_assoc_int ~> gcd.assoc

  zero_zle_int ~> of_nat_0_le_iff

  lcm_dvd2_nat ~> dvd_lcm2

  lcm_dvd2_int ~> dvd_lcm2

  lcm_dvd1_nat ~> dvd_lcm1

  lcm_dvd1_int ~> dvd_lcm1

  gcd_zero_nat ~> gcd_eq_0_iff

  gcd_zero_int ~> gcd_eq_0_iff

  gcd_dvd2_nat ~> gcd_dvd2

  gcd_dvd2_int ~> gcd_dvd2

  gcd_dvd1_nat ~> gcd_dvd1

  gcd_dvd1_int ~> gcd_dvd1

  int_numeral ~> of_nat_numeral

  lcm_ac_nat ~> ac_simps

  lcm_ac_int ~> ac_simps

  gcd_ac_nat ~> ac_simps

  gcd_ac_int ~> ac_simps

  abs_int_eq ~> abs_of_nat

  zless_int ~> of_nat_less_iff

  zdiff_int ~> of_nat_diff

  zadd_int ~> of_nat_add

  int_mult ~> of_nat_mult

  int_Suc ~> of_nat_Suc

  inj_int ~> inj_of_nat

  int_1 ~> of_nat_1

  int_0 ~> of_nat_0

  Lcm_empty_nat ~> Lcm_empty

  Lcm_empty_int ~> Lcm_empty

  Lcm_insert_nat ~> Lcm_insert

  Lcm_insert_int ~> Lcm_insert

  comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd

  comp_fun_idem_gcd_int ~> comp_fun_idem_gcd

  comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm

  comp_fun_idem_lcm_int ~> comp_fun_idem_lcm

  Lcm_eq_0 ~> Lcm_eq_0_I

  Lcm0_iff ~> Lcm_0_iff

  Lcm_dvd_int ~> Lcm_least

  divides_mult_nat ~> divides_mult

  divides_mult_int ~> divides_mult

  lcm_0_nat ~> lcm_0_right

  lcm_0_int ~> lcm_0_right

  lcm_0_left_nat ~> lcm_0_left

  lcm_0_left_int ~> lcm_0_left

  dvd_gcd_D1_nat ~> dvd_gcdD1

  dvd_gcd_D1_int ~> dvd_gcdD1

  dvd_gcd_D2_nat ~> dvd_gcdD2

  dvd_gcd_D2_int ~> dvd_gcdD2

  coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff

  coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff

  realpow_minus_mult ~> power_minus_mult

  realpow_Suc_le_self ~> power_Suc_le_self

  dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest

INCOMPATIBILITY.

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

* Renamed HOL/Quotient_Examples/FSet.thy to

HOL/Quotient_Examples/Quotient_FSet.thy

INCOMPATIBILITY.

*** ML ***

* ML antiquotation @{path} is superseded by @{file}, which ensures that

the argument is a plain file. Minor INCOMPATIBILITY.

* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML

library (notably for big integers). Subtle change of semantics:

Integer.gcd and Integer.lcm both normalize the sign, results are never

negative. This coincides with the definitions in HOL/GCD.thy.

INCOMPATIBILITY.

* Structure Rat for rational numbers is now an integral part of

Isabelle/ML, with special notation @int/nat or @int for numerals (an

abbreviation for antiquotation @{Pure.rat argument}) and ML pretty

printing. Standard operations on type Rat.rat are provided via ad-hoc

overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to

use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been

superseded by General.Div.

* The ML function "ML" provides easy access to run-time compilation.

This is particularly useful for conditional compilation, without

requiring separate files.

* Low-level ML system structures (like PolyML and RunCall) are no longer

exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.

* Antiquotation @{make_string} is available during Pure bootstrap --

with approximative output quality.

* Option ML_exception_debugger controls detailed exception trace via the

Poly/ML debugger. Relevant ML modules need to be compiled beforehand

with ML_file_debug, or with ML_file and option ML_debugger enabled. Note

debugger information requires consirable time and space: main

Isabelle/HOL with full debugger support may need ML_system_64.

* Local_Theory.restore has been renamed to Local_Theory.reset to

emphasize its disruptive impact on the cumulative context, notably the

scope of 'private' or 'qualified' names. Note that Local_Theory.reset is

only appropriate when targets are managed, e.g. starting from a global

theory and returning to it. Regular definitional packages should use

balanced blocks of Local_Theory.open_target versus

Local_Theory.close_target instead. Rare INCOMPATIBILITY.

* Structure TimeLimit (originally from the SML/NJ library) has been

replaced by structure Timeout, with slightly different signature.

INCOMPATIBILITY.

* Discontinued cd and pwd operations, which are not well-defined in a

multi-threaded environment. Note that files are usually located

relatively to the master directory of a theory (see also

File.full_path). Potential INCOMPATIBILITY.

* Binding.empty_atts supersedes Thm.empty_binding and

Attrib.empty_binding. Minor INCOMPATIBILITY.

*** System ***

* Many Isabelle tools that require a Java runtime system refer to the

settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,

depending on the underlying platform. The settings for "isabelle build"

ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been

discontinued. Potential INCOMPATIBILITY.

* The Isabelle system environment always ensures that the main

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

"isabelle_scala_script".

* Isabelle tools may consist of .scala files: the Scala compiler is

invoked on the spot. The source needs to define some object that extends

Isabelle_Tool.Body.

* The Isabelle ML process is now managed directly by Isabelle/Scala, and

shell scripts merely provide optional command-line access. In

particular:

  . Scala module ML_Process to connect to the raw ML process,

    with interaction via stdin/stdout/stderr or in batch mode;

  . command-line tool "isabelle console" as interactive wrapper;

  . command-line tool "isabelle process" as batch mode wrapper.

* The executable "isabelle_process" has been discontinued. Tools and

prover front-ends should use ML_Process or Isabelle_Process in

Isabelle/Scala. INCOMPATIBILITY.

* New command-line tool "isabelle process" supports ML evaluation of

literal expressions (option -e) or files (option -f) in the context of a

given heap image. Errors lead to premature exit of the ML process with

return code 1.

* Command-line tool "isabelle console" provides option -r to help to

bootstrapping Isabelle/Pure interactively.

* Command-line tool "isabelle yxml" has been discontinued.

INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in

Isabelle/ML or Isabelle/Scala.

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

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

produce robust shell scripts under program control, without worrying

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

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

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

been discontinued.

* SML/NJ and old versions of Poly/ML are no longer supported.

* Poly/ML heaps now follow the hierarchy of sessions, and thus require

much less disk space.

* System option "checkpoint" helps to fine-tune the global heap space

management of isabelle build. This is relevant for big sessions that may

exhaust the small 32-bit address space of the ML process (which is used

by default).

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