NEWS

'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

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

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

*** General ***

* Command 'ML_file' evaluates ML text from a file directly within the
theory, without any predeclaration via 'uses' in the theory header.

* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
is called fastforce / fast_force_tac already since Isabelle2011-1.

* Updated and extended "isar-ref" manual, reduced remaining material
in old "ref" manual.


*** Pure ***

* Code generation for Haskell: restrict unqualified imports from
Haskell Prelude to a small set of fundamental operations.

* Command "export_code": relative file names are interpreted
relatively to master directory of current theory rather than
the rather arbitrary current working directory.
INCOMPATIBILITY.

* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN", or explicit proof
structure instead.  Note that Isabelle/ML provides a variety of
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.

* Command 'typ' supports an additional variant with explicit sort
constraint, to infer and check the most general type conforming to a
given given sort.  Example (in HOL):

  typ "_ * _ * bool * unit" :: finite


*** HOL ***

* Library/Debug.thy and Library/Parallel.thy: debugging and parallel
execution for code generated towards Isabelle/ML.

* Simproc "finite_Collect" rewrites set comprehensions into pointfree
expressions.

* Quickcheck:

  - added an optimisation for equality premises.
    It is switched on by default, and can be switched off by setting
    the configuration quickcheck_optimise_equality to false.    

* The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option "z3_with_extensions".
Minor INCOMPATIBILITY.

* Sledgehammer:

  - Added MaSh relevance filter based on machine-learning; see the
    Sledgehammer manual for details.
  - Rationalized type encodings ("type_enc" option).
  - Renamed options:
      max_relevant ~> max_facts
      relevance_thresholds ~> fact_thresholds


*** Document preparation ***

* Default for \<euro> is now based on eurosym package, instead of
slightly exotic babel/greek.

* Document variant NAME may use different LaTeX entry point
document/root_NAME.tex if that file exists, instead of the common
document/root.tex.

* Simplified custom document/build script, instead of old-style
document/IsaMakefile.  Minor INCOMPATIBILITY.


*** System ***

* Advanced support for Isabelle sessions and build management, see
"system" manual for the chapter of that name, especially the "isabelle
build" tool and its examples.  INCOMPATIBILITY, isabelle usedir /
mkdir / make are rendered obsolete.

* Discontinued obsolete "isabelle makeall".

* Discontinued obsolete IsaMakefile and ROOT.ML files from the
Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that
provides some traditional targets that invoke "isabelle build".  Note
that this is inefficient!  Applications of Isabelle/HOL involving
"isabelle make" should be upgraded to use "isabelle build" directly.

* Discontinued obsolete Isabelle/build script, it is superseded by the
regular isabelle build tool.  For example:

  isabelle build -s -b HOLCF

* The "isabelle options" tool prints Isabelle system options, as
required for "isabelle build", for example.

* The "isabelle mkroot" tool prepares session root directories for use
with "isabelle build", similar to former "isabelle mkdir" for
"isabelle usedir".

* The "isabelle components" tool helps to resolve add-on components
that are not bundled, or referenced from a bare-bones repository
version of Isabelle.

* Discontinued support for Poly/ML 5.2.1, which was the last version
without exception positions and advanced ML compiler/toplevel
configuration.

* Discontinued special treatment of Proof General -- no longer guess
PROOFGENERAL_HOME based on accidental file-system layout.  Minor
INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS
settings manually, or use a Proof General version that has been
bundled as Isabelle component.


New in Isabelle2012 (May 2012)
------------------------------

*** General ***

* Prover IDE (PIDE) improvements:

  - more robust Sledgehammer integration (as before the sledgehammer
    command-line needs to be typed into the source buffer)
  - markup for bound variables
  - markup for types of term variables (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)

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

* Auxiliary contexts indicate block structure for specifications with
additional parameters and assumptions.  Such unnamed contexts may be
nested within other targets, like 'theory', 'locale', 'class',
'instantiation' etc.  Results from the local context are generalized
accordingly and applied to the enclosing target context.  Example:

  context
    fixes x y z :: 'a
    assumes xy: "x = y" and yz: "y = z"
  begin

  lemma my_trans: "x = z" using xy yz by simp

  end

  thm my_trans

The most basic application is to factor-out context elements of
several fixes/assumes/shows theorem statements, e.g. see
~~/src/HOL/Isar_Examples/Group_Context.thy

Any other local theory specification element works within the "context
... begin ... end" block as well.

* Bundled declarations associate attributed fact expressions with a
given name in the context.  These may be later included in other
contexts.  This allows to manage context extensions casually, without
the logical dependencies of locales and locale interpretation.  See
commands 'bundle', 'include', 'including' etc. in the isar-ref manual.

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

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

* New tutorial "Programming and Proving in Isabelle/HOL"
("prog-prove").  It completely supersedes "A Tutorial Introduction to
Structured Isar Proofs" ("isar-overview"), which has been removed.  It
also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
Logic" as the recommended beginners tutorial, but does not cover all
of the material of that old tutorial.

* Updated and extended reference manuals: "isar-ref",
"implementation", "system"; reduced remaining material in old "ref"
manual.


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

* 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 occurrence (!)"

* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
tolerant against multiple unifiers, as long as the final result is
unique.  (As before, rules are composed in canonical right-to-left
order to accommodate newly introduced premises.)

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

* Discontinued configuration option "syntax_positions": atomic terms
in parse trees are always annotated by position constraints.

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

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

* Discontinued old "prems" fact, which used to refer to the accidental
collection of foundational premises in the context (already marked as
legacy since Isabelle2011).


*** HOL ***

* 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 some set S that has
been accidentally used as predicates by "%x. x : S", and some
predicate P that has been accidentally used as set 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 mix 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

* The representation of numerals has changed.  Datatype "num"
represents strictly positive binary numerals, along with functions
"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
positive and negated numeric literals, respectively.  See also
definitions in ~~/src/HOL/Num.thy.  Potential INCOMPATIBILITY, some
user theories may require adaptations as follows:

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

* Transfer: New package intended to generalize the existing
"descending" method and related theorem attributes from the Quotient
package.  (Not all functionality is implemented yet, but future
development will focus on Transfer as an eventual replacement for the
corresponding parts of the Quotient package.)

  - transfer_rule attribute: Maintains a collection of transfer rules,
    which relate constants at two different types. Transfer rules may
    relate different type instances of the same polymorphic constant,
    or they may relate an operation on a raw type to a corresponding
    operation on an abstract type (quotient or subtype). For example:

    ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
    (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int

  - transfer method: Replaces a subgoal on abstract types with an
    equivalent subgoal on the corresponding raw types. Constants are
    replaced with corresponding ones according to the transfer rules.
    Goals are generalized over all free variables by default; this is
    necessary for variables whose types change, but can be overridden
    for specific variables with e.g. "transfer fixing: x y z".  The
    variant transfer' method allows replacing a subgoal with one that
    is logically stronger (rather than equivalent).

  - relator_eq attribute: Collects identity laws for relators of
    various type constructors, e.g. "list_all2 (op =) = (op =)".  The
    transfer method uses these lemmas to infer transfer rules for
    non-polymorphic constants on the fly.

  - transfer_prover method: Assists with proving a transfer rule for a
    new constant, provided the constant is defined in terms of other
    constants that already have transfer rules. It should be applied
    after unfolding the constant definitions.

  - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
    from type nat to type int.

* Lifting: New package intended to generalize the quotient_definition
facility of the Quotient package; designed to work with Transfer.

  - lift_definition command: Defines operations on an abstract type in
    terms of a corresponding operation on a representation
    type.  Example syntax:

    lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
      is List.insert

    Users must discharge a respectfulness proof obligation when each
    constant is defined. (For a type copy, i.e. a typedef with UNIV,
    the proof is discharged automatically.) The obligation is
    presented in a user-friendly, readable form; a respectfulness
    theorem in the standard format and a transfer rule are generated
    by the package.

  - Integration with code_abstype: For typedefs (e.g. subtypes
    corresponding to a datatype invariant, such as dlist),
    lift_definition generates a code certificate theorem and sets up
    code generation for each constant.

  - setup_lifting command: Sets up the Lifting package to work with a
    user-defined type. The user must provide either a quotient theorem
    or a type_definition theorem.  The package configures transfer
    rules for equality and quantifiers on the type, and sets up the
    lift_definition command to work with the type.

  - Usage examples: See Quotient_Examples/Lift_DList.thy,
    Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,
    Word/Word.thy and Library/Float.thy.

* Quotient package:

  - The 'quotient_type' command now supports a 'morphisms' option with
    rep and abs functions, similar to typedef.

  - 'quotient_type' sets up new types to work with the Lifting and
    Transfer packages, as with 'setup_lifting'.

  - The 'quotient_definition' command now requires the user to prove a
    respectfulness property at the point where the constant is
    defined, similar to lift_definition; INCOMPATIBILITY.

  - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
    accordingly, INCOMPATIBILITY.

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

  - Added "quickcheck_locale" configuration to specify how to process
    conjectures in a locale context.

* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option
and affecting 'rat' and 'real'.

* Sledgehammer:
  - Integrated more tightly with SPASS, as described in the ITP 2012
    paper "More SPASS with Isabelle".
  - Made it try "smt" as a fallback if "metis" fails or times out.
  - Added support for the following provers: Alt-Ergo (via Why3 and
    TFF1), iProver, iProver-Eq.
  - Sped up the minimizer.
  - 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 "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.

* New "eventually_elim" method as a generalized variant of the
eventually_elim* rules.  Supports structured proofs.

* Typedef with implicit set definition is considered legacy.  Use
"typedef (open)" form instead, which will eventually become the
default.

* Record: code generation can be switched off manually with

  declare [[record_coden = false]]  -- "default true"

* Datatype: type parameters allow explicit sort constraints.

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

* Clarified attribute "mono_set": pure declaration without modifying
the result of the fact expression.

* 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 ~> relcomp_unfold
  symp_def ~> (modified, 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.

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

* Theory Relation: Consolidated constant name for relation composition
and corresponding theorem names:

  - Renamed constant rel_comp to relcomp.

  - Dropped abbreviation pred_comp. Use relcompp instead.

  - Renamed theorems:

    rel_compI ~> relcompI
    rel_compEpair ~> relcompEpair
    rel_compE ~> relcompE
    pred_comp_rel_comp_eq ~> relcompp_relcomp_eq
    rel_comp_empty1 ~> relcomp_empty1
    rel_comp_mono ~> relcomp_mono
    rel_comp_subset_Sigma ~> relcomp_subset_Sigma
    rel_comp_distrib ~> relcomp_distrib
    rel_comp_distrib2 ~> relcomp_distrib2
    rel_comp_UNION_distrib ~> relcomp_UNION_distrib
    rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
    single_valued_rel_comp ~> single_valued_relcomp
    rel_comp_def ~> relcomp_unfold
    converse_rel_comp ~> converse_relcomp
    pred_compI ~> relcomppI
    pred_compE ~> relcomppE
    pred_comp_bot1 ~> relcompp_bot1
    pred_comp_bot2 ~> relcompp_bot2
    transp_pred_comp_less_eq ~> transp_relcompp_less_eq
    pred_comp_mono ~> relcompp_mono
    pred_comp_distrib ~> relcompp_distrib
    pred_comp_distrib2 ~> relcompp_distrib2
    converse_pred_comp ~> converse_relcompp

    finite_rel_comp ~> finite_relcomp

    set_rel_comp ~> set_relcomp

INCOMPATIBILITY.

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

* Finite_Set.fold now qualified.  INCOMPATIBILITY.

* Consolidated theorem names concerning fold combinators:

  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
  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.simps (in point-free formulation)
  foldr_fold_rev ~> foldr_conv_fold
  foldl_fold ~> foldl_conv_fold
  foldr_foldr ~> foldr_conv_foldl
  foldl_foldr ~> foldl_conv_foldr
  fold_set_remdups ~> fold_set_fold_remdups
  fold_set ~> fold_set_fold
  fold1_set ~> fold1_set_fold

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, foldl_assoc,
foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can be
useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
unfolding "foldr_conv_fold" and "foldl_conv_fold".

* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding
lemmas over fold rather than foldr, or make use of lemmas
fold_conv_foldr and fold_rev.

* Congruence rules Option.map_cong and Option.bind_cong for recursion
through option types.

* "Transitive_Closure.ntrancl": bounded transitive closure on
relations.

* Constant "Set.not_member" now qualified.  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

* Theory Library/Multiset: Improved code generation of multisets.

* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
are expressed via type classes again. The special syntax
\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
setsum_set, which is now subsumed by Big_Operators.setsum.
INCOMPATIBILITY.

* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
use theory HOL/Library/Nat_Bijection instead.

* Theory HOL/Library/RBT_Impl: Backing implementation of red-black
trees is now inside a type class context.  Names of affected
operations and lemmas have been prefixed by rbt_.  INCOMPATIBILITY for
theories working directly with raw red-black trees, adapt the names as
follows:

  Operations:
  bulkload -> rbt_bulkload
  del_from_left -> rbt_del_from_left
  del_from_right -> rbt_del_from_right
  del -> rbt_del
  delete -> rbt_delete
  ins -> rbt_ins
  insert -> rbt_insert
  insertw -> rbt_insert_with
  insert_with_key -> rbt_insert_with_key
  map_entry -> rbt_map_entry
  lookup -> rbt_lookup
  sorted -> rbt_sorted
  tree_greater -> rbt_greater
  tree_less -> rbt_less
  tree_less_symbol -> rbt_less_symbol
  union -> rbt_union
  union_with -> rbt_union_with
  union_with_key -> rbt_union_with_key

  Lemmas:
  balance_left_sorted -> balance_left_rbt_sorted
  balance_left_tree_greater -> balance_left_rbt_greater
  balance_left_tree_less -> balance_left_rbt_less
  balance_right_sorted -> balance_right_rbt_sorted
  balance_right_tree_greater -> balance_right_rbt_greater
  balance_right_tree_less -> balance_right_rbt_less
  balance_sorted -> balance_rbt_sorted
  balance_tree_greater -> balance_rbt_greater
  balance_tree_less -> balance_rbt_less
  bulkload_is_rbt -> rbt_bulkload_is_rbt
  combine_sorted -> combine_rbt_sorted
  combine_tree_greater -> combine_rbt_greater
  combine_tree_less -> combine_rbt_less
  delete_in_tree -> rbt_delete_in_tree
  delete_is_rbt -> rbt_delete_is_rbt
  del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
  del_from_left_tree_less -> rbt_del_from_left_rbt_less
  del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
  del_from_right_tree_less -> rbt_del_from_right_rbt_less
  del_in_tree -> rbt_del_in_tree
  del_inv1_inv2 -> rbt_del_inv1_inv2
  del_sorted -> rbt_del_rbt_sorted
  del_tree_greater -> rbt_del_rbt_greater
  del_tree_less -> rbt_del_rbt_less
  dom_lookup_Branch -> dom_rbt_lookup_Branch
  entries_lookup -> entries_rbt_lookup
  finite_dom_lookup -> finite_dom_rbt_lookup
  insert_sorted -> rbt_insert_rbt_sorted
  insertw_is_rbt -> rbt_insertw_is_rbt
  insertwk_is_rbt -> rbt_insertwk_is_rbt
  insertwk_sorted -> rbt_insertwk_rbt_sorted
  insertw_sorted -> rbt_insertw_rbt_sorted
  ins_sorted -> ins_rbt_sorted
  ins_tree_greater -> ins_rbt_greater
  ins_tree_less -> ins_rbt_less
  is_rbt_sorted -> is_rbt_rbt_sorted
  lookup_balance -> rbt_lookup_balance
  lookup_bulkload -> rbt_lookup_rbt_bulkload
  lookup_delete -> rbt_lookup_rbt_delete
  lookup_Empty -> rbt_lookup_Empty
  lookup_from_in_tree -> rbt_lookup_from_in_tree
  lookup_in_tree -> rbt_lookup_in_tree
  lookup_ins -> rbt_lookup_ins
  lookup_insert -> rbt_lookup_rbt_insert
  lookup_insertw -> rbt_lookup_rbt_insertw
  lookup_insertwk -> rbt_lookup_rbt_insertwk
  lookup_keys -> rbt_lookup_keys
  lookup_map -> rbt_lookup_map
  lookup_map_entry -> rbt_lookup_rbt_map_entry
  lookup_tree_greater -> rbt_lookup_rbt_greater
  lookup_tree_less -> rbt_lookup_rbt_less
  lookup_union -> rbt_lookup_rbt_union
  map_entry_color_of -> rbt_map_entry_color_of
  map_entry_inv1 -> rbt_map_entry_inv1
  map_entry_inv2 -> rbt_map_entry_inv2
  map_entry_is_rbt -> rbt_map_entry_is_rbt
  map_entry_sorted -> rbt_map_entry_rbt_sorted
  map_entry_tree_greater -> rbt_map_entry_rbt_greater
  map_entry_tree_less -> rbt_map_entry_rbt_less
  map_tree_greater -> map_rbt_greater
  map_tree_less -> map_rbt_less
  map_sorted -> map_rbt_sorted
  paint_sorted -> paint_rbt_sorted
  paint_lookup -> paint_rbt_lookup
  paint_tree_greater -> paint_rbt_greater
  paint_tree_less -> paint_rbt_less
  sorted_entries -> rbt_sorted_entries
  tree_greater_eq_trans -> rbt_greater_eq_trans
  tree_greater_nit -> rbt_greater_nit
  tree_greater_prop -> rbt_greater_prop
  tree_greater_simps -> rbt_greater_simps
  tree_greater_trans -> rbt_greater_trans
  tree_less_eq_trans -> rbt_less_eq_trans
  tree_less_nit -> rbt_less_nit
  tree_less_prop -> rbt_less_prop
  tree_less_simps -> rbt_less_simps
  tree_less_trans -> rbt_less_trans
  tree_ord_props -> rbt_ord_props
  union_Branch -> rbt_union_Branch
  union_is_rbt -> rbt_union_is_rbt
  unionw_is_rbt -> rbt_unionw_is_rbt
  unionwk_is_rbt -> rbt_unionwk_is_rbt
  unionwk_sorted -> rbt_unionwk_rbt_sorted

* Theory HOL/Library/Float: Floating point numbers are now defined as
a subset of the real numbers.  All operations are defined using the
lifing-framework and proofs use the transfer method.  INCOMPATIBILITY.

  Changed Operations:
  float_abs -> abs
  float_nprt -> nprt
  float_pprt -> pprt
  pow2 -> use powr
  round_down -> float_round_down
  round_up -> float_round_up
  scale -> exponent

  Removed Operations:
  ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod

  Renamed Lemmas:
  abs_float_def -> Float.compute_float_abs
  bitlen_ge0 -> bitlen_nonneg
  bitlen.simps -> Float.compute_bitlen
  float_components -> Float_mantissa_exponent
  float_divl.simps -> Float.compute_float_divl
  float_divr.simps -> Float.compute_float_divr
  float_eq_odd -> mult_powr_eq_mult_powr_iff
  float_power -> real_of_float_power
  lapprox_posrat_def -> Float.compute_lapprox_posrat
  lapprox_rat.simps -> Float.compute_lapprox_rat
  le_float_def' -> Float.compute_float_le
  le_float_def -> less_eq_float.rep_eq
  less_float_def' -> Float.compute_float_less
  less_float_def -> less_float.rep_eq
  normfloat_def -> Float.compute_normfloat
  normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0
  normfloat -> normfloat_def
  normfloat_unique -> use normfloat_def
  number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral
  one_float_def -> Float.compute_float_one
  plus_float_def -> Float.compute_float_plus
  rapprox_posrat_def -> Float.compute_rapprox_posrat
  rapprox_rat.simps -> Float.compute_rapprox_rat
  real_of_float_0 -> zero_float.rep_eq
  real_of_float_1 -> one_float.rep_eq
  real_of_float_abs -> abs_float.rep_eq
  real_of_float_add -> plus_float.rep_eq
  real_of_float_minus -> uminus_float.rep_eq
  real_of_float_mult -> times_float.rep_eq
  real_of_float_simp -> Float.rep_eq
  real_of_float_sub -> minus_float.rep_eq
  round_down.simps -> Float.compute_float_round_down
  round_up.simps -> Float.compute_float_round_up
  times_float_def -> Float.compute_float_times
  uminus_float_def -> Float.compute_float_uminus
  zero_float_def -> Float.compute_float_zero

  Lemmas not necessary anymore, use the transfer method:
  bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,
  float_divr, float_le_simp, float_less1_mantissa_bound,
  float_less_simp, float_less_zero, float_le_zero,
  float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,
  floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,
  lapprox_rat_bottom, normalized_float, rapprox_posrat,
  rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,
  real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
  round_up, zero_le_float, zero_less_float

* New theory HOL/Library/DAList provides an abstract type for
association lists with distinct keys.

* Session HOL/IMP: Added new theory of abstract interpretation of
annotated commands.

* Session HOL-Import: Re-implementation from scratch is faster,
simpler, and more scalable.  Requires a proof bundle, which is
available as an external component.  Discontinued old (and mostly
dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.

* 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

* Session HOL-Word: New proof method "word_bitwise" for splitting
machine word equalities and inequalities into logical circuits,
defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
multiplication, shifting by constants, bitwise operators and numeric
constants.  Requires fixed-length word types, not 'a word.  Solves
many standard word identities outright and converts more into first
order problems amenable to blast or similar.  See also examples in
HOL/Word/Examples/WordExamples.thy.

* Session HOL-Probability: Introduced the type "'a measure" to
represent measures, this replaces the records 'a algebra and 'a
measure_space.  The locales based on subset_class now have two
locale-parameters the space \<Omega> and the set of measurable sets M.
The product of probability spaces uses now the same constant as the
finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
measure".  Most constants are defined now outside of locales and gain
an additional parameter, like null_sets, almost_eventually or \<mu>'.
Measure space constructions for distributions and densities now got
their own constants distr and density.  Instead of using locales to
describe measure spaces with a finite space, the measure count_space
and point_measure is introduced.  INCOMPATIBILITY.

  Renamed constants:
  measure -> emeasure
  finite_measure.\<mu>' -> measure
  product_algebra_generator -> prod_algebra
  product_prob_space.emb -> prod_emb
  product_prob_space.infprod_algebra -> PiM

  Removed locales:
  completeable_measure_space
  finite_measure_space
  finite_prob_space
  finite_product_finite_prob_space
  finite_product_sigma_algebra
  finite_sigma_algebra
  measure_space
  pair_finite_prob_space
  pair_finite_sigma_algebra
  pair_finite_space
  pair_sigma_algebra
  product_sigma_algebra

  Removed constants:
  conditional_space
  distribution -> use distr measure, or distributed predicate
  image_space
  joint_distribution -> use distr measure, or distributed predicate
  pair_measure_generator
  product_prob_space.infprod_algebra -> use PiM
  subvimage

  Replacement theorems:
  finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite
  finite_measure.empty_measure -> measure_empty
  finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq
  finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq
  finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably
  finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
  finite_measure.finite_measure -> finite_measure.emeasure_finite
  finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton
  finite_measure.positive_measure' -> measure_nonneg
  finite_measure.real_measure -> finite_measure.emeasure_real
  finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb
  finite_product_sigma_algebra.in_P -> sets_PiM_I_finite
  finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty
  information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed
  information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple
  information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple
  information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple
  information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple
  information_space.entropy_commute -> information_space.entropy_commute_simple
  information_space.entropy_eq -> information_space.entropy_simple_distributed
  information_space.entropy_generic_eq -> information_space.entropy_simple_distributed
  information_space.entropy_positive -> information_space.entropy_nonneg_simple
  information_space.entropy_uniform_max -> information_space.entropy_uniform
  information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq
  information_space.KL_eq_0 -> information_space.KL_same_eq_0
  information_space.KL_ge_0 -> information_space.KL_nonneg
  information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed
  information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple
  Int_stable_cuboids -> Int_stable_atLeastAtMost
  Int_stable_product_algebra_generator -> positive_integral
  measure_preserving -> equality "distr M N f = N" "f : measurable M N"
  measure_space.additive -> emeasure_additive
  measure_space.AE_iff_null_set -> AE_iff_null
  measure_space.almost_everywhere_def -> eventually_ae_filter
  measure_space.almost_everywhere_vimage -> AE_distrD
  measure_space.continuity_from_above -> INF_emeasure_decseq
  measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
  measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
  measure_space.continuity_from_below -> SUP_emeasure_incseq
  measure_space_density -> emeasure_density
  measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
  measure_space.integrable_vimage -> integrable_distr
  measure_space.integral_translated_density -> integral_density
  measure_space.integral_vimage -> integral_distr
  measure_space.measure_additive -> plus_emeasure
  measure_space.measure_compl -> emeasure_compl
  measure_space.measure_countable_increasing -> emeasure_countable_increasing
  measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
  measure_space.measure_decseq -> decseq_emeasure
  measure_space.measure_Diff -> emeasure_Diff
  measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
  measure_space.measure_eq_0 -> emeasure_eq_0
  measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite
  measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
  measure_space.measure_incseq -> incseq_emeasure
  measure_space.measure_insert -> emeasure_insert
  measure_space.measure_mono -> emeasure_mono
  measure_space.measure_not_negative -> emeasure_not_MInf
  measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
  measure_space.measure_setsum -> setsum_emeasure
  measure_space.measure_setsum_split -> setsum_emeasure_cover
  measure_space.measure_space_vimage -> emeasure_distr
  measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
  measure_space.measure_subadditive -> subadditive
  measure_space.measure_top -> emeasure_space
  measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
  measure_space.measure_Un_null_set -> emeasure_Un_null_set
  measure_space.positive_integral_translated_density -> positive_integral_density
  measure_space.positive_integral_vimage -> positive_integral_distr
  measure_space.real_continuity_from_above -> Lim_measure_decseq
  measure_space.real_continuity_from_below -> Lim_measure_incseq
  measure_space.real_measure_countably_subadditive -> measure_subadditive_countably
  measure_space.real_measure_Diff -> measure_Diff
  measure_space.real_measure_finite_Union -> measure_finite_Union
  measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
  measure_space.real_measure_subadditive -> measure_subadditive
  measure_space.real_measure_Union -> measure_Union
  measure_space.real_measure_UNION -> measure_UNION
  measure_space.simple_function_vimage -> simple_function_comp
  measure_space.simple_integral_vimage -> simple_integral_distr
  measure_space.simple_integral_vimage -> simple_integral_distr
  measure_unique_Int_stable -> measure_eqI_generator_eq
  measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
  pair_sigma_algebra.measurable_cut_fst -> sets_Pair1
  pair_sigma_algebra.measurable_cut_snd -> sets_Pair2
  pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1
  pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2
  pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff
  pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap
  pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'
  pair_sigma_algebra.sets_swap -> sets_pair_swap
  pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
  pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
  pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
  pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
  pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
  pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
  prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
  prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
  prob_space.measure_space_1 -> prob_space.emeasure_space_1
  prob_space.prob_space_vimage -> prob_space_distr
  prob_space.random_variable_restrict -> measurable_restrict
  prob_space_unique_Int_stable -> measure_eqI_prob_space
  product_algebraE -> prod_algebraE_all
  product_algebra_generator_der -> prod_algebra_eq_finite
  product_algebra_generator_into_space -> prod_algebra_sets_into_space
  product_algebraI -> sets_PiM_I_finite
  product_measure_exists -> product_sigma_finite.sigma_finite
  product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator
  product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb
  product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty
  product_prob_space.measurable_component -> measurable_component_singleton
  product_prob_space.measurable_emb -> measurable_prod_emb
  product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single
  product_prob_space.measurable_singleton_infprod -> measurable_component_singleton
  product_prob_space.measure_emb -> emeasure_prod_emb
  product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
  product_sigma_algebra.product_algebra_into_space -> space_closed
  product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
  product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
  product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
  sequence_space.measure_infprod -> sequence_space.measure_PiM_countable
  sets_product_algebra -> sets_PiM
  sigma_algebra.measurable_sigma -> measurable_measure_of
  sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
  sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
  sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
  space_product_algebra -> space_PiM

* Session HOL-TPTP: support to parse and import TPTP problems (all
languages) into Isabelle/HOL.


*** FOL ***

* New "case_product" attribute (see HOL).


*** ZF ***

* Greater support for structured proofs involving induction or case
analysis.

* Much greater use of mathematical symbols.

* Removal of many ML theorem bindings.  INCOMPATIBILITY.


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


*** System ***

* USER_HOME settings variable points to cross-platform user home
directory, which coincides with HOME on POSIX systems only.  Likewise,
the Isabelle path specification "~" now expands to $USER_HOME, instead
of former $HOME.  A different default for USER_HOME may be set
explicitly in shell environment, before Isabelle settings are
evaluated.  Minor INCOMPATIBILITY: need to adapt Isabelle path where
the generic user home was intended.

* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
notation, which is useful for the jEdit file browser, for example.

* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
(not just JRE).



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