Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

*** General ***

* Prover IDE (PIDE) improvements:

  - markup for bound variables

  - markup for types of term variables (e.g. displayed as tooltips)

  - support for user-defined Isar commands within the running session

  - improved support for Unicode outside original 16bit range

    e.g. glyph for \<A> (thanks to jEdit 4.5.1)

* Updated and extended reference manuals ("isar-ref" and

"implementation"); reduced remaining material in old "ref" manual.

* Rule attributes in local theory declarations (e.g. locale or class)

are now statically evaluated: the resulting theorem is stored instead

of the original expression.  INCOMPATIBILITY in rare situations, where

the historic accident of dynamic re-evaluation in interpretations

etc. was exploited.

* Commands 'lemmas' and 'theorems' allow local variables using 'for'

declaration, and results are standardized before being stored.  Thus

old-style "standard" after instantiation or composition of facts

becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of

indices of schematic variables.

* Renamed some inner syntax categories:

    num ~> num_token

    xnum ~> xnum_token

    xstr ~> str_token

Minor INCOMPATIBILITY.  Note that in practice "num_const" or

"num_position" etc. are mainly used instead (which also include

position information via constraints).

* Simplified configuration options for syntax ambiguity: see

"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

manual.  Minor INCOMPATIBILITY.

* Forward declaration of outer syntax keywords within the theory

header -- minor INCOMPATIBILITY for user-defined commands.  Allow new

commands to be used in the same theory where defined.

* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar

(not just JRE).

*** Pure ***

* Command 'definition' no longer exports the foundational "raw_def"

into the user context.  Minor INCOMPATIBILITY, may use the regular

"def" result with attribute "abs_def" to imitate the old version.

* Attribute "abs_def" turns an equation of the form "f x y == t" into

"f == %x y. t", which ensures that "simp" or "unfold" steps always

expand it.  This also works for object-logic equality.  (Formerly

undocumented feature.)

* Discontinued old "prems" fact, which used to refer to the accidental

collection of foundational premises in the context (marked as legacy

since Isabelle2011).

* Obsolete command 'types' has been discontinued.  Use 'type_synonym'

instead.  INCOMPATIBILITY.

* Ancient code generator for SML and its commands 'code_module',

'code_library', 'consts_code', 'types_code' have been discontinued.

Use commands of the generic code generator instead.  INCOMPATIBILITY.

* Redundant attribute 'code_inline' has been discontinued. Use

'code_unfold' instead.  INCOMPATIBILITY.

* Dropped attribute 'code_unfold_post' in favor of the its dual

'code_abbrev', which yields a common pattern in definitions like

  definition [code_abbrev]: "f = t"

INCOMPATIBILITY.

* Sort constraints are now propagated in simultaneous statements, just

like type constraints.  INCOMPATIBILITY in rare situations, where

distinct sorts used to be assigned accidentally.  For example:

  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"

  lemma "P (x::'a)" and "Q (y::'a::bar)"

    -- "now uniform 'a::bar instead of default sort for first occurence (!)"

*** HOL ***

* The representation of numerals has changed. We now have a datatype

"num" representing strictly positive binary numerals, along with

functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to

represent positive and negated numeric literals, respectively. (See

definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories

may require adaptations:

  - Theorems with number_ring or number_semiring constraints: These

    classes are gone; use comm_ring_1 or comm_semiring_1 instead.

  - Theories defining numeric types: Remove number, number_semiring,

    and number_ring instances. Defer all theorems about numerals until

    after classes one and semigroup_add have been instantiated.

  - Numeral-only simp rules: Replace each rule having a "number_of v"

    pattern with two copies, one for numeral and one for neg_numeral.

  - Theorems about subclasses of semiring_1 or ring_1: These classes

    automatically support numerals now, so more simp rules and

    simprocs may now apply within the proof.

  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:

    Redefine using other integer operations.

* Type 'a set is now a proper type constructor (just as before

Isabelle2008).  Definitions mem_def and Collect_def have disappeared.

Non-trivial INCOMPATIBILITY.  For developments keeping predicates and

sets separate, it is often sufficient to rephrase sets S accidentally

used as predicates by "%x. x : S" and predicates P accidentally used

as sets by "{x. P x}".  Corresponding proofs in a first step should be

pruned from any tinkering with former theorems mem_def and

Collect_def as far as possible.

For developments which deliberately mixed predicates and

sets, a planning step is necessary to determine what should become a

predicate and what a set.  It can be helpful to carry out that step in

Isabelle2011-1 before jumping right into the current release.

* Code generation by default implements sets as container type rather

than predicates.  INCOMPATIBILITY.

* New type synonym 'a rel = ('a * 'a) set

* Theory Divides: Discontinued redundant theorems about div and mod.

INCOMPATIBILITY, use the corresponding generic theorems instead.

  DIVISION_BY_ZERO ~> div_by_0, mod_by_0

  zdiv_self ~> div_self

  zmod_self ~> mod_self

  zdiv_zero ~> div_0

  zmod_zero ~> mod_0

  zdiv_zmod_equality ~> div_mod_equality2

  zdiv_zmod_equality2 ~> div_mod_equality

  zmod_zdiv_trivial ~> mod_div_trivial

  zdiv_zminus_zminus ~> div_minus_minus

  zmod_zminus_zminus ~> mod_minus_minus

  zdiv_zminus2 ~> div_minus_right

  zmod_zminus2 ~> mod_minus_right

  zdiv_minus1_right ~> div_minus1_right

  zmod_minus1_right ~> mod_minus1_right

  zdvd_mult_div_cancel ~> dvd_mult_div_cancel

  zmod_zmult1_eq ~> mod_mult_right_eq

  zpower_zmod ~> power_mod

  zdvd_zmod ~> dvd_mod

  zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd

  mod_mult_distrib ~> mult_mod_left

  mod_mult_distrib2 ~> mult_mod_right

* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use

generic mult_2 and mult_2_right instead. INCOMPATIBILITY.

* More default pred/set conversions on a couple of relation operations

and predicates.  Added powers of predicate relations.

Consolidation of some relation theorems:

  converse_def ~> converse_unfold

  rel_comp_def ~> rel_comp_unfold

  symp_def ~> (dropped, use symp_def and sym_def instead)

  transp_def ~> transp_trans

  Domain_def ~> Domain_unfold

  Range_def ~> Domain_converse [symmetric]

Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

See theory "Relation" for examples for making use of pred/set conversions

by means of attributes "to_set" and "to_pred".

INCOMPATIBILITY.

* Consolidated various theorem names relating to Finite_Set.fold

combinator:

  inf_INFI_fold_inf ~> inf_INF_fold_inf

  sup_SUPR_fold_sup ~> sup_SUP_fold_sup

  INFI_fold_inf ~> INF_fold_inf

  SUPR_fold_sup ~> SUP_fold_sup

  union_set ~> union_set_fold

  minus_set ~> minus_set_fold

INCOMPATIBILITY.

* Consolidated theorem names concerning fold combinators:

  INFI_set_fold ~> INF_set_fold

  SUPR_set_fold ~> SUP_set_fold

  INF_code ~> INF_set_foldr

  SUP_code ~> SUP_set_foldr

  foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)

  foldl.simps ~> foldl_Nil foldl_Cons

  foldr_fold_rev ~> foldr_def

  foldl_fold ~> foldl_def

INCOMPATIBILITY.

* Dropped rarely useful theorems concerning fold combinators:

foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,

rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,

concat_conv_foldl, foldl_weak_invariant, foldl_invariant,

foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,

listsum_conv_fold, listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.

Prefer "List.fold" with canonical argument order, or boil down

"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"

and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"

and "List.foldl plus 0", prefer "List.listsum".

* Congruence rules Option.map_cong and Option.bind_cong for recursion

through option types.

* Concrete syntax for case expressions includes constraints for source

positions, and thus produces Prover IDE markup for its bindings.

INCOMPATIBILITY for old-style syntax translations that augment the

pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of

one_case.

* Discontinued configuration option "syntax_positions": atomic terms

in parse trees are always annotated by position constraints.

* Finite_Set.fold now qualified.  INCOMPATIBILITY.

* Renamed some facts on canonical fold on lists, in order to avoid

problems with interpretation involving corresponding facts on foldl

with the same base names:

  fold_set_remdups ~> fold_set_fold_remdups

  fold_set ~> fold_set_fold

  fold1_set ~> fold1_set_fold

INCOMPATIBILITY.

* Renamed facts about the power operation on relations, i.e., relpow

  to match the constant's name:

  rel_pow_1 ~> relpow_1

  rel_pow_0_I ~> relpow_0_I

  rel_pow_Suc_I ~> relpow_Suc_I

  rel_pow_Suc_I2 ~> relpow_Suc_I2

  rel_pow_0_E ~> relpow_0_E

  rel_pow_Suc_E ~> relpow_Suc_E

  rel_pow_E ~> relpow_E

  rel_pow_Suc_D2 ~> relpow_Suc_D2

  rel_pow_Suc_E2 ~> relpow_Suc_E2 

  rel_pow_Suc_D2' ~> relpow_Suc_D2'

  rel_pow_E2 ~> relpow_E2

  rel_pow_add ~> relpow_add

  rel_pow_commute ~> relpow

  rel_pow_empty ~> relpow_empty:

  rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow

  rel_pow_imp_rtrancl ~> relpow_imp_rtrancl

  rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow

  rtrancl_imp_rel_pow ~> rtrancl_imp_relpow

  rel_pow_fun_conv ~> relpow_fun_conv

  rel_pow_finite_bounded1 ~> relpow_finite_bounded1

  rel_pow_finite_bounded ~> relpow_finite_bounded

  rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow

  trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow

  single_valued_rel_pow ~> single_valued_relpow

INCOMPATIBILITY.

* New theory HOL/Library/DAList provides an abstract type for association

  lists with distinct keys.

* 'datatype' specifications allow explicit sort constraints.

* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,

use theory HOL/Library/Nat_Bijection instead.

* Session HOL-Word: Discontinued many redundant theorems specific to

type 'a word. INCOMPATIBILITY, use the corresponding generic theorems

instead.

  word_sub_alt ~> word_sub_wi

  word_add_alt ~> word_add_def

  word_mult_alt ~> word_mult_def

  word_minus_alt ~> word_minus_def

  word_0_alt ~> word_0_wi

  word_1_alt ~> word_1_wi

  word_add_0 ~> add_0_left

  word_add_0_right ~> add_0_right

  word_mult_1 ~> mult_1_left

  word_mult_1_right ~> mult_1_right

  word_add_commute ~> add_commute

  word_add_assoc ~> add_assoc

  word_add_left_commute ~> add_left_commute

  word_mult_commute ~> mult_commute

  word_mult_assoc ~> mult_assoc

  word_mult_left_commute ~> mult_left_commute

  word_left_distrib ~> left_distrib

  word_right_distrib ~> right_distrib

  word_left_minus ~> left_minus

  word_diff_0_right ~> diff_0_right

  word_diff_self ~> diff_self

  word_sub_def ~> diff_minus

  word_diff_minus ~> diff_minus

  word_add_ac ~> add_ac

  word_mult_ac ~> mult_ac

  word_plus_ac0 ~> add_0_left add_0_right add_ac

  word_times_ac1 ~> mult_1_left mult_1_right mult_ac

  word_order_trans ~> order_trans

  word_order_refl ~> order_refl

  word_order_antisym ~> order_antisym

  word_order_linear ~> linorder_linear

  lenw1_zero_neq_one ~> zero_neq_one

  word_number_of_eq ~> number_of_eq

  word_of_int_add_hom ~> wi_hom_add

  word_of_int_sub_hom ~> wi_hom_sub

  word_of_int_mult_hom ~> wi_hom_mult

  word_of_int_minus_hom ~> wi_hom_neg

  word_of_int_succ_hom ~> wi_hom_succ

  word_of_int_pred_hom ~> wi_hom_pred

  word_of_int_0_hom ~> word_0_wi

  word_of_int_1_hom ~> word_1_wi

* Clarified attribute "mono_set": pure declaration without modifying

the result of the fact expression.

* "Transitive_Closure.ntrancl": bounded transitive closure on

relations.

* Constant "Set.not_member" now qualified.  INCOMPATIBILITY.

* "sublists" moved to theory More_List.  INCOMPATIBILITY.

* Theory Int: Discontinued many legacy theorems specific to type int.

INCOMPATIBILITY, use the corresponding generic theorems instead.

  zminus_zminus ~> minus_minus

  zminus_0 ~> minus_zero

  zminus_zadd_distrib ~> minus_add_distrib

  zadd_commute ~> add_commute

  zadd_assoc ~> add_assoc

  zadd_left_commute ~> add_left_commute

  zadd_ac ~> add_ac

  zmult_ac ~> mult_ac

  zadd_0 ~> add_0_left

  zadd_0_right ~> add_0_right

  zadd_zminus_inverse2 ~> left_minus

  zmult_zminus ~> mult_minus_left

  zmult_commute ~> mult_commute

  zmult_assoc ~> mult_assoc

  zadd_zmult_distrib ~> left_distrib

  zadd_zmult_distrib2 ~> right_distrib

  zdiff_zmult_distrib ~> left_diff_distrib

  zdiff_zmult_distrib2 ~> right_diff_distrib

  zmult_1 ~> mult_1_left

  zmult_1_right ~> mult_1_right

  zle_refl ~> order_refl

  zle_trans ~> order_trans

  zle_antisym ~> order_antisym

  zle_linear ~> linorder_linear

  zless_linear ~> linorder_less_linear

  zadd_left_mono ~> add_left_mono

  zadd_strict_right_mono ~> add_strict_right_mono

  zadd_zless_mono ~> add_less_le_mono

  int_0_less_1 ~> zero_less_one

  int_0_neq_1 ~> zero_neq_one

  zless_le ~> less_le

  zpower_zadd_distrib ~> power_add

  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

  zero_le_zpower_abs ~> zero_le_power_abs

* Theory Deriv: Renamed

  DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

* New "case_product" attribute to generate a case rule doing multiple

case distinctions at the same time.  E.g.

  list.exhaust [case_product nat.exhaust]

produces a rule which can be used to perform case distinction on both

a list and a nat.

* Improved code generation of multisets.

* New diagnostic command find_unused_assms to find potentially superfluous

  assumptions in theorems using Quickcheck.

* Quickcheck:

  - Quickcheck returns variable assignments as counterexamples, which

    allows to reveal the underspecification of functions under test.

    For example, refuting "hd xs = x", it presents the variable

    assignment xs = [] and x = a1 as a counterexample, assuming that

    any property is false whenever "hd []" occurs in it.

    These counterexample are marked as potentially spurious, as

    Quickcheck also returns "xs = []" as a counterexample to the

    obvious theorem "hd xs = hd xs".

    After finding a potentially spurious counterexample, Quickcheck

    continues searching for genuine ones.

    By default, Quickcheck shows potentially spurious and genuine

    counterexamples. The option "genuine_only" sets quickcheck to

    only show genuine counterexamples.

  - The command 'quickcheck_generator' creates random and exhaustive

    value generators for a given type and operations.

    It generates values by using the operations as if they were

    constructors of that type. 

  - Support for multisets.

  - Added "use_subtype" options.

* Nitpick:

  - Fixed infinite loop caused by the 'peephole_optim' option and

    affecting 'rat' and 'real'.

* Sledgehammer:

  - Added "lam_trans", "uncurry_aliases", and "minimize" options.

  - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").

  - Renamed "sound" option to "strict".

* Metis:

  - Added possibility to specify lambda translations scheme as a

    parenthesized argument (e.g., "by (metis (lifting) ...)").

* SMT:

  - renamed "smt_fixed" option to "smt_read_only_certificates".

* Command 'try0':

  - Renamed from 'try_methods'. INCOMPATIBILITY.

* New "eventually_elim" method as a generalized variant of the

  eventually_elim* rules. Supports structured proofs.

*** FOL ***

* New "case_product" attribute (see HOL).

*** ML ***

* Antiquotation @{keyword "name"} produces a parser for outer syntax

from a minor keyword introduced via theory header declaration.

* Antiquotation @{command_spec "name"} produces the

Outer_Syntax.command_spec from a major keyword introduced via theory

header declaration; it can be passed to Outer_Syntax.command etc.

* Local_Theory.define no longer hard-wires default theorem name

"foo_def", but retains the binding as given.  If that is Binding.empty

/ Attrib.empty_binding, the result is not registered as user-level

fact.  The Local_Theory.define_internal variant allows to specify a

non-empty name (used for the foundation in the background theory),

while omitting the fact binding in the user-context.  Potential

INCOMPATIBILITY for derived definitional packages: need to specify

naming policy for primitive definitions more explicitly.

* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in

conformance with similar operations in structure Term and Logic.

* Antiquotation @{attributes [...]} embeds attribute source

representation into the ML text, which is particularly useful with

declarations like Local_Theory.note.

* Structure Proof_Context follows standard naming scheme.  Old

ProofContext has been discontinued.  INCOMPATIBILITY.

* Refined Local_Theory.declaration {syntax, pervasive}, with subtle

change of semantics: update is applied to auxiliary local theory

context as well.

* Modernized some old-style infix operations:

  addeqcongs    ~> Simplifier.add_eqcong

  deleqcongs    ~> Simplifier.del_eqcong

  addcongs      ~> Simplifier.add_cong

  delcongs      ~> Simplifier.del_cong

  setmksimps    ~> Simplifier.set_mksimps

  setmkcong     ~> Simplifier.set_mkcong

  setmksym      ~> Simplifier.set_mksym

  setmkeqTrue   ~> Simplifier.set_mkeqTrue

  settermless   ~> Simplifier.set_termless

  setsubgoaler  ~> Simplifier.set_subgoaler

  addsplits     ~> Splitter.add_split

  delsplits     ~> Splitter.del_split

New in Isabelle2011-1 (October 2011)

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

*** General ***

* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as

"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.

  - Management of multiple theory files directly from the editor

    buffer store -- bypassing the file-system (no requirement to save

    files for checking).

  - Markup of formal entities within the text buffer, with semantic

    highlighting, tooltips and hyperlinks to jump to defining source

    positions.

  - Improved text rendering, with sub/superscripts in the source

    buffer (including support for copy/paste wrt. output panel, HTML

    theory output and other non-Isabelle text boxes).

  - Refined scheduling of proof checking and printing of results,

    based on interactive editor view.  (Note: jEdit folding and

    narrowing allows to restrict buffer perspectives explicitly.)

  - Reduced CPU performance requirements, usable on machines with few

    cores.

  - Reduced memory requirements due to pruning of unused document

    versions (garbage collection).

See also ~~/src/Tools/jEdit/README.html for further information,

including some remaining limitations.

* Theory loader: source files are exclusively located via the master

directory of each theory node (where the .thy file itself resides).

The global load path (such as src/HOL/Library) has been discontinued.

Note that the path element ~~ may be used to reference theories in the

Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".

INCOMPATIBILITY.

* Theory loader: source files are identified by content via SHA1

digests.  Discontinued former path/modtime identification and optional

ISABELLE_FILE_IDENT plugin scripts.

* Parallelization of nested Isar proofs is subject to

Goal.parallel_proofs_threshold (default 100).  See also isabelle

usedir option -Q.

* Name space: former unsynchronized references are now proper

configuration options, with more conventional names:

  long_names   ~> names_long

  short_names  ~> names_short

  unique_names ~> names_unique

Minor INCOMPATIBILITY, need to declare options in context like this:

  declare [[names_unique = false]]

* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note

that the result needs to be unique, which means fact specifications

may have to be refined after enriching a proof context.

* Attribute "case_names" has been refined: the assumptions in each case

can be named now by following the case name with [name1 name2 ...].

* Isabelle/Isar reference manual has been updated and extended:

  - "Synopsis" provides a catalog of main Isar language concepts.

  - Formal references in syntax diagrams, via @{rail} antiquotation.

  - Updated material from classic "ref" manual, notably about

    "Classical Reasoner".

*** HOL ***

* Class bot and top require underlying partial order rather than

preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.

* Class complete_lattice: generalized a couple of lemmas from sets;

generalized theorems INF_cong and SUP_cong.  New type classes for

complete boolean algebras and complete linear orders.  Lemmas

Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in

class complete_linorder.

Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,

Sup_fun_def, Inf_apply, Sup_apply.

Removed redundant lemmas (the right hand side gives hints how to

replace them for (metis ...), or (simp only: ...) proofs):

  Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]

  Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]

  Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right

  Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right

  Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right

  Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right

  Inter_def ~> INF_def, image_def

  Union_def ~> SUP_def, image_def

  INT_eq ~> INF_def, and image_def

  UN_eq ~> SUP_def, and image_def

  INF_subset ~> INF_superset_mono [OF _ order_refl]

More consistent and comprehensive names:

  INTER_eq_Inter_image ~> INF_def

  UNION_eq_Union_image ~> SUP_def

  INFI_def ~> INF_def

  SUPR_def ~> SUP_def

  INF_leI ~> INF_lower

  INF_leI2 ~> INF_lower2

  le_INFI ~> INF_greatest

  le_SUPI ~> SUP_upper

  le_SUPI2 ~> SUP_upper2

  SUP_leI ~> SUP_least

  INFI_bool_eq ~> INF_bool_eq

  SUPR_bool_eq ~> SUP_bool_eq

  INFI_apply ~> INF_apply

  SUPR_apply ~> SUP_apply

  INTER_def ~> INTER_eq

  UNION_def ~> UNION_eq

INCOMPATIBILITY.

* Renamed theory Complete_Lattice to Complete_Lattices.

INCOMPATIBILITY.

* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,

INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,

Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,

Sup_insert are now declared as [simp].  INCOMPATIBILITY.

* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,

compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,

sup_inf_absob, sup_left_idem are now declared as [simp].  Minor

INCOMPATIBILITY.

* Added syntactic classes "inf" and "sup" for the respective

constants.  INCOMPATIBILITY: Changes in the argument order of the

(mostly internal) locale predicates for some derived classes.

* Theorem collections ball_simps and bex_simps do not contain theorems

referring to UNION any longer; these have been moved to collection

UN_ball_bex_simps.  INCOMPATIBILITY.

* Theory Archimedean_Field: floor now is defined as parameter of a

separate type class floor_ceiling.

* Theory Finite_Set: more coherent development of fold_set locales:

    locale fun_left_comm ~> locale comp_fun_commute

    locale fun_left_comm_idem ~> locale comp_fun_idem

Both use point-free characterization; interpretation proofs may need

adjustment.  INCOMPATIBILITY.

* Theory Limits: Type "'a net" has been renamed to "'a filter", in

accordance with standard mathematical terminology. INCOMPATIBILITY.

* Theory Complex_Main: The locale interpretations for the

bounded_linear and bounded_bilinear locales have been removed, in

order to reduce the number of duplicate lemmas. Users must use the

original names for distributivity theorems, potential INCOMPATIBILITY.

  divide.add ~> add_divide_distrib

  divide.diff ~> diff_divide_distrib

  divide.setsum ~> setsum_divide_distrib

  mult.add_right ~> right_distrib

  mult.diff_right ~> right_diff_distrib

  mult_right.setsum ~> setsum_right_distrib

  mult_left.diff ~> left_diff_distrib

* Theory Complex_Main: Several redundant theorems have been removed or

replaced by more general versions. INCOMPATIBILITY.

  real_diff_def ~> minus_real_def

  real_divide_def ~> divide_real_def

  real_less_def ~> less_le

  real_abs_def ~> abs_real_def

  real_sgn_def ~> sgn_real_def

  real_mult_commute ~> mult_commute

  real_mult_assoc ~> mult_assoc

  real_mult_1 ~> mult_1_left

  real_add_mult_distrib ~> left_distrib

  real_zero_not_eq_one ~> zero_neq_one

  real_mult_inverse_left ~> left_inverse

  INVERSE_ZERO ~> inverse_zero

  real_le_refl ~> order_refl

  real_le_antisym ~> order_antisym

  real_le_trans ~> order_trans

  real_le_linear ~> linear

  real_le_eq_diff ~> le_iff_diff_le_0

  real_add_left_mono ~> add_left_mono

  real_mult_order ~> mult_pos_pos

  real_mult_less_mono2 ~> mult_strict_left_mono

  real_of_int_real_of_nat ~> real_of_int_of_nat_eq

  real_0_le_divide_iff ~> zero_le_divide_iff

  realpow_two_disj ~> power2_eq_iff

  real_squared_diff_one_factored ~> square_diff_one_factored

  realpow_two_diff ~> square_diff_square_factored

  reals_complete2 ~> complete_real

  real_sum_squared_expand ~> power2_sum

  exp_ln_eq ~> ln_unique

  expi_add ~> exp_add

  expi_zero ~> exp_zero

  lemma_DERIV_subst ~> DERIV_cong

  LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

  LIMSEQ_const ~> tendsto_const

  LIMSEQ_norm ~> tendsto_norm

  LIMSEQ_add ~> tendsto_add

  LIMSEQ_minus ~> tendsto_minus

  LIMSEQ_minus_cancel ~> tendsto_minus_cancel

  LIMSEQ_diff ~> tendsto_diff

  bounded_linear.LIMSEQ ~> bounded_linear.tendsto

  bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

  LIMSEQ_mult ~> tendsto_mult

  LIMSEQ_inverse ~> tendsto_inverse

  LIMSEQ_divide ~> tendsto_divide

  LIMSEQ_pow ~> tendsto_power

  LIMSEQ_setsum ~> tendsto_setsum

  LIMSEQ_setprod ~> tendsto_setprod

  LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

  LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

  LIMSEQ_imp_rabs ~> tendsto_rabs

  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

  LIMSEQ_Complex ~> tendsto_Complex

  LIM_ident ~> tendsto_ident_at

  LIM_const ~> tendsto_const

  LIM_add ~> tendsto_add

  LIM_add_zero ~> tendsto_add_zero

  LIM_minus ~> tendsto_minus

  LIM_diff ~> tendsto_diff

  LIM_norm ~> tendsto_norm

  LIM_norm_zero ~> tendsto_norm_zero

  LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

  LIM_norm_zero_iff ~> tendsto_norm_zero_iff

  LIM_rabs ~> tendsto_rabs

  LIM_rabs_zero ~> tendsto_rabs_zero

  LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

  LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

  LIM_compose ~> tendsto_compose

  LIM_mult ~> tendsto_mult

  LIM_scaleR ~> tendsto_scaleR

  LIM_of_real ~> tendsto_of_real

  LIM_power ~> tendsto_power

  LIM_inverse ~> tendsto_inverse

  LIM_sgn ~> tendsto_sgn

  isCont_LIM_compose ~> isCont_tendsto_compose

  bounded_linear.LIM ~> bounded_linear.tendsto

  bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

  bounded_bilinear.LIM ~> bounded_bilinear.tendsto

  bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

  bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

  bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

  LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

* Theory Complex_Main: The definition of infinite series was

generalized.  Now it is defined on the type class {topological_space,

comm_monoid_add}.  Hence it is useable also for extended real numbers.

* Theory Complex_Main: The complex exponential function "expi" is now

a type-constrained abbreviation for "exp :: complex => complex"; thus

several polymorphic lemmas about "exp" are now applicable to "expi".

* Code generation:

  - Theory Library/Code_Char_ord provides native ordering of

    characters in the target language.

  - Commands code_module and code_library are legacy, use export_code

    instead.

  - Method "evaluation" is legacy, use method "eval" instead.

  - Legacy evaluator "SML" is deactivated by default.  May be

    reactivated by the following theory command:

      setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}

* Declare ext [intro] by default.  Rare INCOMPATIBILITY.

* New proof method "induction" that gives induction hypotheses the

name "IH", thus distinguishing them from further hypotheses that come

from rule induction.  The latter are still called "hyps".  Method

"induction" is a thin wrapper around "induct" and follows the same

syntax.

* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is

still available as a legacy feature for some time.

* Nitpick:

  - Added "need" and "total_consts" options.

  - Reintroduced "show_skolems" option by popular demand.

  - Renamed attribute: nitpick_def ~> nitpick_unfold.

    INCOMPATIBILITY.

* Sledgehammer:

  - Use quasi-sound (and efficient) translations by default.

  - Added support for the following provers: E-ToFoF, LEO-II,

    Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.

  - Automatically preplay and minimize proofs before showing them if

    this can be done within reasonable time.

  - sledgehammer available_provers ~> sledgehammer supported_provers.

    INCOMPATIBILITY.

  - Added "preplay_timeout", "slicing", "type_enc", "sound",

    "max_mono_iters", and "max_new_mono_instances" options.

  - Removed "explicit_apply" and "full_types" options as well as "Full

    Types" Proof General menu item. INCOMPATIBILITY.

* Metis:

  - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.

  - Obsoleted "metisFT" -- use "metis (full_types)" instead.

    INCOMPATIBILITY.

* Command 'try':

  - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and

    "elim:" options. INCOMPATIBILITY.

  - Introduced 'try' that not only runs 'try_methods' but also

    'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.

* Quickcheck:

  - Added "eval" option to evaluate terms for the found counterexample

    (currently only supported by the default (exhaustive) tester).

  - Added post-processing of terms to obtain readable counterexamples

    (currently only supported by the default (exhaustive) tester).

  - New counterexample generator quickcheck[narrowing] enables

    narrowing-based testing.  Requires the Glasgow Haskell compiler

    with its installation location defined in the Isabelle settings

    environment as ISABELLE_GHC.

  - Removed quickcheck tester "SML" based on the SML code generator

    (formly in HOL/Library).

* Function package: discontinued option "tailrec".  INCOMPATIBILITY,

use 'partial_function' instead.

* Theory Library/Extended_Reals replaces now the positive extended

reals found in probability theory. This file is extended by

Multivariate_Analysis/Extended_Real_Limits.

* Theory Library/Old_Recdef: old 'recdef' package has been moved here,

from where it must be imported explicitly if it is really required.

INCOMPATIBILITY.

* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has

been moved here.  INCOMPATIBILITY.

* Theory Library/Saturated provides type of numbers with saturated

arithmetic.

* Theory Library/Product_Lattice defines a pointwise ordering for the

product type 'a * 'b, and provides instance proofs for various order

and lattice type classes.

* Theory Library/Countable now provides the "countable_datatype" proof

method for proving "countable" class instances for datatypes.

* Theory Library/Cset_Monad allows do notation for computable sets

(cset) via the generic monad ad-hoc overloading facility.

* Library: Theories of common data structures are split into theories

for implementation, an invariant-ensuring type, and connection to an

abstract type. INCOMPATIBILITY.

  - RBT is split into RBT and RBT_Mapping.

  - AssocList is split and renamed into AList and AList_Mapping.

  - DList is split into DList_Impl, DList, and DList_Cset.

  - Cset is split into Cset and List_Cset.

* Theory Library/Nat_Infinity has been renamed to

Library/Extended_Nat, with name changes of the following types and

constants:

  type inat   ~> type enat

  Fin         ~> enat

  Infty       ~> infinity (overloaded)

  iSuc        ~> eSuc

  the_Fin     ~> the_enat

Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has

been renamed accordingly. INCOMPATIBILITY.

* Session Multivariate_Analysis: The euclidean_space type class now

fixes a constant "Basis :: 'a set" consisting of the standard

orthonormal basis for the type. Users now have the option of

quantifying over this set instead of using the "basis" function, e.g.

"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".

* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed

to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants

"Cart_nth" and "Cart_lambda" have been respectively renamed to

"vec_nth" and "vec_lambda"; theorems mentioning those names have

changed to match. Definition theorems for overloaded constants now use

the standard "foo_vec_def" naming scheme. A few other theorems have

been renamed as follows (INCOMPATIBILITY):

  Cart_eq          ~> vec_eq_iff

  dist_nth_le_cart ~> dist_vec_nth_le

  tendsto_vector   ~> vec_tendstoI

  Cauchy_vector    ~> vec_CauchyI

* Session Multivariate_Analysis: Several duplicate theorems have been

removed, and other theorems have been renamed or replaced with more

general versions. INCOMPATIBILITY.

  finite_choice ~> finite_set_choice

  eventually_conjI ~> eventually_conj

  eventually_and ~> eventually_conj_iff

  eventually_false ~> eventually_False

  setsum_norm ~> norm_setsum

  Lim_sequentially ~> LIMSEQ_def

  Lim_ident_at ~> LIM_ident

  Lim_const ~> tendsto_const

  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

  Lim_neg ~> tendsto_minus

  Lim_add ~> tendsto_add

  Lim_sub ~> tendsto_diff

  Lim_mul ~> tendsto_scaleR

  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

  Lim_linear ~> bounded_linear.tendsto

  Lim_component ~> tendsto_euclidean_component

  Lim_component_cart ~> tendsto_vec_nth

  Lim_inner ~> tendsto_inner [OF tendsto_const]

  dot_lsum ~> inner_setsum_left

  dot_rsum ~> inner_setsum_right

  continuous_cmul ~> continuous_scaleR [OF continuous_const]

  continuous_neg ~> continuous_minus

  continuous_sub ~> continuous_diff

  continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

  continuous_mul ~> continuous_scaleR

  continuous_inv ~> continuous_inverse

  continuous_at_within_inv ~> continuous_at_within_inverse

  continuous_at_inv ~> continuous_at_inverse

  continuous_at_norm ~> continuous_norm [OF continuous_at_id]

  continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

  continuous_at_component ~> continuous_component [OF continuous_at_id]

  continuous_on_neg ~> continuous_on_minus

  continuous_on_sub ~> continuous_on_diff

  continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

  continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

  continuous_on_mul ~> continuous_on_scaleR

  continuous_on_mul_real ~> continuous_on_mult

  continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

  continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

  continuous_on_inverse ~> continuous_on_inv

  uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

  uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

  subset_interior ~> interior_mono

  subset_closure ~> closure_mono

  closure_univ ~> closure_UNIV

  real_arch_lt ~> reals_Archimedean2

  real_arch ~> reals_Archimedean3

  real_abs_norm ~> abs_norm_cancel

  real_abs_sub_norm ~> norm_triangle_ineq3

  norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

* Session HOL-Probability:

  - Caratheodory's extension lemma is now proved for ring_of_sets.

  - Infinite products of probability measures are now available.

  - Sigma closure is independent, if the generator is independent

  - Use extended reals instead of positive extended

    reals. INCOMPATIBILITY.

* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

  expand_fun_below ~> fun_below_iff

  below_fun_ext ~> fun_belowI

  expand_cfun_eq ~> cfun_eq_iff

  ext_cfun ~> cfun_eqI

  expand_cfun_below ~> cfun_below_iff

  below_cfun_ext ~> cfun_belowI

  monofun_fun_fun ~> fun_belowD

  monofun_fun_arg ~> monofunE

  monofun_lub_fun ~> adm_monofun [THEN admD]

  cont_lub_fun ~> adm_cont [THEN admD]

  cont2cont_Rep_CFun ~> cont2cont_APP

  cont_Rep_CFun_app ~> cont_APP_app

  cont_Rep_CFun_app_app ~> cont_APP_app_app

  cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]

  cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]

  contlub_cfun ~> lub_APP [symmetric]

  contlub_LAM ~> lub_LAM [symmetric]

  thelubI ~> lub_eqI

  UU_I ~> bottomI

  lift_distinct1 ~> lift.distinct(1)

  lift_distinct2 ~> lift.distinct(2)

  Def_not_UU ~> lift.distinct(2)

  Def_inject ~> lift.inject

  below_UU_iff ~> below_bottom_iff

  eq_UU_iff ~> eq_bottom_iff

*** Document preparation ***

* Antiquotation @{rail} layouts railroad syntax diagrams, see also

isar-ref manual, both for description and actual application of the

same.