NEWS

more NEWS and CONTRIBUTORS;

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

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

*** General ***

* Uniform management of "quick_and_dirty" as system option (see also
"isabelle options"), configuration option within the context (see also
Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
INCOMPATIBILITY, need to use more official Isabelle means to access
quick_and_dirty, instead of historical poking into mutable reference.

* Renamed command 'print_configs' to 'print_options'.  Minor
INCOMPATIBILITY.

* Sessions may be organized via 'chapter' specifications in the ROOT
file, which determines a two-level hierarchy of browser info.  The old
tree-like organization via implicit sub-session relation, with its
tendency towards erratic fluctuation of URLs, has been discontinued.
The default chapter is "Unsorted".  Potential INCOMPATIBILITY for HTML
presentation of theories.

* Discontinued obsolete 'uses' within theory header.  Note that
commands like 'ML_file' work without separate declaration of file
dependencies.  Minor INCOMPATIBILITY.

* Discontinued redundant 'use' command, which was superseded by
'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.

* Updated and extended "isar-ref" and "implementation" manual,
eliminated old "ref" manual.

* Proper diagnostic command 'print_state'.  Old 'pr' (with its
implicit change of some global references) is retained for now as
control command, e.g. for ProofGeneral 3.7.x.

* Discontinued 'print_drafts' command with its old-fashioned PS output
and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
'display_drafts' instead and print via the regular document viewer.


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

* Improved "Theories" panel: Continuous checking of proof document
(visible and required parts) may be controlled explicitly, using check
box or shortcut "C+e ENTER".  Individual theory nodes may be marked
explicitly as required and checked in full, using check box or
shortcut "C+e SPACE".

* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.

* Support for asynchronous print functions, as overlay to existing
document content.

* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.

* Dockable window "Documentation" provides access to Isabelle
documentation.

* Dockable window "Timing" provides an overview of relevant command
timing information.

* Option to skip over proofs, using implicit 'sorry' internally.


*** Pure ***

* Type theory is now immutable, without any special treatment of
drafts or linear updates (which could lead to "stale theory" errors in
the past).  Discontinued obsolete operations like Theory.copy,
Theory.checkpoint, and the auxiliary type theory_ref.  Minor
INCOMPATIBILITY.

* System option "proofs" has been discontinued.  Instead the global
state of Proofterm.proofs is persistently compiled into logic images
as required, notably HOL-Proofs.  Users no longer need to change
Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.

* Syntax translation functions (print_translation etc.) always depend
on Proof.context.  Discontinued former "(advanced)" option -- this is
now the default.  Minor INCOMPATIBILITY.

* Target-sensitive commands 'interpretation' and 'sublocale'.
Particulary, 'interpretation' now allows for non-persistent
interpretation within "context ... begin ... end" blocks.
See "isar-ref" manual for details.

* Improved locales diagnostic command 'print_dependencies'.

* Discontinued obsolete 'axioms' command, which has been marked as
legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
instead, while observing its uniform scope for polymorphism.

* Discontinued empty name bindings in 'axiomatization'.
INCOMPATIBILITY.

* SELECT_GOAL now retains the syntactic context of the overall goal
state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
situations.


*** HOL ***

* Improved support for adhoc overloading of constants (see also
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.
Use explicit 'code equation' and 'code abstract' to distinguish both when desired.

* Code generator:
  * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
  * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
    subsuming 'code_modulename'.
  See the Isar reference manual for syntax diagrams, and the HOL theories for examples.

* Library/Polynomial.thy:
  * Use lifting for primitive definitions.
  * Explicit conversions from and to lists of coefficients, used for generated code.
  * Replaced recursion operator poly_rec by fold_coeffs.
  * Prefer pre-existing gcd operation for gcd.
  * Fact renames:
    poly_eq_iff ~> poly_eq_poly_eq_iff
    poly_ext ~> poly_eqI
    expand_poly_eq ~> poly_eq_iff
IMCOMPATIBILTIY.

* Reification and reflection:
  * Reification is now directly available in HOL-Main in structure "Reification".
  * Reflection now handles multiple lists with variables also.
  * The whole reflection stack has been decomposed into conversions.
INCOMPATIBILITY.

* Weaker precendence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations.  INCOMPATIBILITY.

* Nested case expressions are now translated in a separate check
  phase rather than during parsing. The data for case combinators
  is separated from the datatype package. The declaration attribute
  "case_translation" can be used to register new case combinators:

  declare [[case_translation case_combinator constructor1 ... constructorN]]

* Notation "{p:A. P}" now allows tuple patterns as well.

* Revised devices for recursive definitions over finite sets:
  - Only one fundamental fold combinator on finite set remains:
    Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
    This is now identity on infinite sets.
  - Locales ("mini packages") for fundamental definitions with
    Finite_Set.fold: folding, folding_idem.
  - Locales comm_monoid_set, semilattice_order_set and
    semilattice_neutr_order_set for big operators on sets.
    See theory Big_Operators for canonical examples.
    Note that foundational constants comm_monoid_set.F and
    semilattice_set.F correspond to former combinators fold_image
    and fold1 respectively.  These are now gone.  You may use
    those foundational constants as substitutes, but it is
    preferable to interpret the above locales accordingly. 
  - Dropped class ab_semigroup_idem_mult (special case of lattice,
    no longer needed in connection with Finite_Set.fold etc.)
  - Fact renames:
      card.union_inter ~> card_Un_Int [symmetric]
      card.union_disjoint ~> card_Un_disjoint

INCOMPATIBILITY.

* Locale hierarchy for abstract orderings and (semi)lattices.

* Discontinued theory src/HOL/Library/Eval_Witness.
INCOMPATIBILITY.

* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
Isabelle2013).  Use "isabelle build" to operate on Isabelle sessions.

* Numeric types mapped by default to target language numerals:
natural (replaces former code_numeral) and integer (replaces
former code_int).  Conversions are available as integer_of_natural /
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML).
INCOMPATIBILITY.

* Discontinued theories Code_Integer and Efficient_Nat by a more
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
Code_Target_Nat and Code_Target_Numeral.  See the tutorial on
code generation for details.  INCOMPATIBILITY.

* Introduce type class "conditionally_complete_lattice": Like a complete
  lattice but does not assume the existence of the top and bottom elements.
  Allows to generalize some lemmas about reals and extended reals.
  Removed SupInf and replaced it by the instantiation of
  conditionally_complete_lattice for real. Renamed lemmas about
  conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
  to cInf_... to avoid hidding of similar complete lattice lemmas.

  Introduce type class linear_continuum as combination of conditionally-complete
  lattices and inner dense linorders which have more than one element.
INCOMPATIBILITY.

* Introduce type classes "no_top" and "no_bot" for orderings without top
  and bottom elements.

* Split dense_linorder into inner_dense_order and no_top, no_bot.

* Complex_Main: Unify and move various concepts from
  HOL-Multivariate_Analysis to HOL-Complex_Main.

 - Introduce type class (lin)order_topology and linear_continuum_topology.
   Allows to generalize theorems about limits and order.
   Instances are reals and extended reals.

 - continuous and continuos_on from Multivariate_Analysis:
   "continuous" is the continuity of a function at a filter.
   "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f".

   Generalized continuity lemmas from isCont to continuous on an arbitrary
   filter.

 - compact from Multivariate_Analysis. Use Bolzano's lemma
   to prove compactness of closed intervals on reals. Continuous functions
   attain infimum and supremum on compact sets. The inverse of a continuous
   function is continuous, when the function is continuous on a compact set.

 - connected from Multivariate_Analysis. Use it to prove the
   intermediate value theorem. Show connectedness of intervals on
   linear_continuum_topology).

 - first_countable_topology from Multivariate_Analysis. Is used to
   show equivalence of properties on the neighbourhood filter of x and on
   all sequences converging to x.

 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems
   from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on
   FDERIV. Add variants of DERIV and FDERIV which are restricted to sets,
   i.e. to represent derivatives from left or right.

 - Removed the within-filter. It is replaced by the principal filter:

     F within X = inf F (principal X)

 - Introduce "at x within U" as a single constant, "at x" is now an
   abbreviation for "at x within UNIV"

 - Introduce named theorem collections tendsto_intros, continuous_intros,
   continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or
   FDERIV_intros) are also available as tendsto_eq_intros (or
   FDERIV_eq_intros) where the right-hand side is replaced by a congruence
   rule. This allows to apply them as intro rules and then proving
   equivalence by the simplifier.

 - Restructured theories in HOL-Complex_Main:

   + Moved RealDef and RComplete into Real

   + Introduced Topological_Spaces and moved theorems about
     topological spaces, filters, limits and continuity to it

   + Renamed RealVector to Real_Vector_Spaces

   + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and
     Limits

   + Moved Ln and Log to Transcendental

   + Moved theorems about continuity from Deriv to Topological_Spaces

 - Remove various auxiliary lemmas.

INCOMPATIBILITY.

* Consolidation of library theories on product orders:

    Product_Lattice ~> Product_Order -- pointwise order on products
    Product_ord ~> Product_Lexorder -- lexicographic order on products

INCOMPATIBILITY.

* Sledgehammer:

  - Renamed option:
      isar_shrink ~> isar_compress

* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.
  
  With HOL-Spec_Check, ML developers can check specifications with the
  ML function check_property. The specifications must be of the form
  "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
  src/HOL/Spec_Check/Examples.thy.


*** HOL-Algebra ***

* Discontinued theories src/HOL/Algebra/abstract and .../poly.
Existing theories should be based on src/HOL/Library/Polynomial
instead.  The latter provides integration with HOL's type classes for
rings.  INCOMPATIBILITY.


*** ML ***

* More uniform naming of goal functions for skipped proofs:

    Skip_Proof.prove  ~>  Goal.prove_sorry
    Skip_Proof.prove_global  ~>  Goal.prove_sorry_global

* Antiquotation @{theory_context A} is similar to @{theory A}, but
presents the result as initial Proof.context.

* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
operate on Proof.context instead of claset, for uniformity with addIs,
addEs, addDs etc. Note that claset_of and put_claset allow to manage
clasets separately from the context.

* Simplifier tactics and tools use proper Proof.context instead of
historic type simpset.  Old-style declarations like addsimps,
addsimprocs etc. operate directly on Proof.context.  Raw type simpset
retains its use as snapshot of the main Simplifier context, using
simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
old tools by making them depend on (ctxt : Proof.context) instead of
(ss : simpset), then turn (simpset_of ctxt) into ctxt.

* Discontinued obsolete ML antiquotations @{claset} and @{simpset}.
INCOMPATIBILITY, use @{context} instead.


*** System ***

* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
"isabelle build" in Isabelle2013.  INCOMPATIBILITY.

* Discontinued obsolete isabelle-process options -f and -u (former
administrative aliases of option -e).  Minor INCOMPATIBILITY.

* Discontinued obsolete isabelle print tool, and PRINT_COMMAND
settings variable.

* Discontinued ISABELLE_DOC_FORMAT settings variable and historic
document formats: dvi.gz, ps, ps.gz -- the default document format is
always pdf.

* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
specify global resources of the JVM process run by isabelle build.

* Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
to run Isabelle/Scala source files as standalone programs.

* Improved "isabelle keywords" tool (for old-style ProofGeneral
keyword tables): use Isabelle/Scala operations, which inspect outer
syntax without requiring to build sessions first.



New in Isabelle2013 (February 2013)
-----------------------------------

*** General ***

* Theorem status about oracles and unfinished/failed future proofs is
no longer printed by default, since it is incompatible with
incremental / parallel checking of the persistent document model.  ML
function Thm.peek_status may be used to inspect a snapshot of the
ongoing evaluation process.  Note that in batch mode --- notably
isabelle build --- the system ensures that future proofs of all
accessible theorems in the theory context are finished (as before).

* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints.  This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.

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

* Old command 'use' command and corresponding keyword 'uses' in the
theory header are legacy features and will be discontinued soon.
Tools that load their additional source files may imitate the
'ML_file' implementation, such that the system can take care of
dependencies properly.

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

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

* Improved support for auxiliary contexts that indicate block structure
for specifications.  Nesting of "context fixes ... context assumes ..."
and "class ... context ...".

* Attribute "consumes" allows a negative value as well, which is
interpreted relatively to the total number of premises of the rule in
the target context.  This form of declaration is stable when exported
from a nested 'context' with additional assumptions.  It is the
preferred form for definitional packages, notably cases/rules produced
in HOL/inductive and HOL/function.

* More informative error messages for Isar proof commands involving
lazy enumerations (method applications etc.).

* Refined 'help' command to retrieve outer syntax commands according
to name patterns (with clickable results).


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

* Parallel terminal proofs ('by') are enabled by default, likewise
proofs that are built into packages like 'datatype', 'function'.  This
allows to "run ahead" checking the theory specifications on the
surface, while the prover is still crunching on internal
justifications.  Unfinished / cancelled proofs are restarted as
required to complete full proof checking eventually.

* Improved output panel with tooltips, hyperlinks etc. based on the
same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
tooltips leads to some window that supports the same recursively,
which can lead to stacks of tooltips as the semantic document content
is explored.  ESCAPE closes the whole stack, individual windows may be
closed separately, or detached to become independent jEdit dockables.

* Improved support for commands that produce graph output: the text
message contains a clickable area to open a new instance of the graph
browser on demand.

* More robust incremental parsing of outer syntax (partial comments,
malformed symbols).  Changing the balance of open/close quotes and
comment delimiters works more conveniently with unfinished situations
that frequently occur in user interaction.

* More efficient painting and improved reactivity when editing large
files.  More scalable management of formal document content.

* Smarter handling of tracing messages: prover process pauses after
certain number of messages per command transaction, with some user
dialog to stop or continue.  This avoids swamping the front-end with
potentially infinite message streams.

* More plugin options and preferences, based on Isabelle/Scala.  The
jEdit plugin option panel provides access to some Isabelle/Scala
options, including tuning parameters for editor reactivity and color
schemes.

* Dockable window "Symbols" provides some editing support for Isabelle
symbols.

* Dockable window "Monitor" shows ML runtime statistics.  Note that
continuous display of the chart slows down the system.

* Improved editing support for control styles: subscript, superscript,
bold, reset of style -- operating on single symbols or text
selections.  Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.

* Actions isabelle.increase-font-size and isabelle.decrease-font-size
adjust the main text area font size, and its derivatives for output,
tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often
need to be adapted to local keyboard layouts.

* More reactive completion popup by default: use \t (TAB) instead of
\n (NEWLINE) to minimize intrusion into regular flow of editing.  See
also "Plugin Options / SideKick / General / Code Completion Options".

* Implicit check and build dialog of the specified logic session
image.  For example, HOL, HOLCF, HOL-Nominal can be produced on
demand, without bundling big platform-dependent heap images in the
Isabelle distribution.

* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
from Oracle provide better multi-platform experience.  This version is
now bundled exclusively with Isabelle.


*** 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 sort.  Example (in HOL):

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

* Command 'locale_deps' visualizes all locales and their relations as
a Hasse diagram.


*** HOL ***

* Sledgehammer:

  - Added MaSh relevance filter based on machine-learning; see the
    Sledgehammer manual for details.
  - Polished Isar proofs generated with "isar_proofs" option.
  - Rationalized type encodings ("type_enc" option).
  - Renamed "kill_provers" subcommand to "kill_all".
  - Renamed options:
      isar_proof ~> isar_proofs
      isar_shrink_factor ~> isar_shrink
      max_relevant ~> max_facts
      relevance_thresholds ~> fact_thresholds

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

* Quotient: only one quotient can be defined by quotient_type
INCOMPATIBILITY.

* Lifting:
  - generation of an abstraction function equation in lift_definition
  - quot_del attribute
  - renamed no_abs_code -> no_code (INCOMPATIBILITY.)

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

* Preprocessing of the code generator rewrites set comprehensions into
pointfree expressions.

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

* Simplified 'typedef' specifications: historical options for implicit
set definition and alternative name have been discontinued.  The
former behavior of "typedef (open) t = A" is now the default, but
written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
accordingly.

* Removed constant "chars"; prefer "Enum.enum" on type "char"
directly.  INCOMPATIBILITY.

* Moved operation product, sublists and n_lists from theory Enum to
List.  INCOMPATIBILITY.

* Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.

* Class "comm_monoid_diff" formalises properties of bounded
subtraction, with natural numbers and multisets as typical instances.

* Added combinator "Option.these" with type "'a option set => 'a set".

* Theory "Transitive_Closure": renamed lemmas

  reflcl_tranclp -> reflclp_tranclp
  rtranclp_reflcl -> rtranclp_reflclp

INCOMPATIBILITY.

* Theory "Rings": renamed lemmas (in class semiring)

  left_distrib ~> distrib_right
  right_distrib ~> distrib_left

INCOMPATIBILITY.

* Generalized the definition of limits:

  - Introduced the predicate filterlim (LIM x F. f x :> G) which
    expresses that when the input values x converge to F then the
    output f x converges to G.

  - Added filters for convergence to positive (at_top) and negative
    infinity (at_bot).

  - Moved infinity in the norm (at_infinity) from
    Multivariate_Analysis to Complex_Main.

  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>
    at_top".

INCOMPATIBILITY.

* Theory "Library/Option_ord" provides instantiation of option type to
lattice type classes.

* Theory "Library/Multiset": renamed

    constant fold_mset ~> Multiset.fold
    fact fold_mset_commute ~> fold_mset_comm

INCOMPATIBILITY.

* Renamed theory Library/List_Prefix to Library/Sublist, with related
changes as follows.

  - Renamed constants (and related lemmas)

      prefix ~> prefixeq
      strict_prefix ~> prefix

  - Replaced constant "postfix" by "suffixeq" with swapped argument
    order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped
    old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.
    Renamed lemmas accordingly.

  - Added constant "list_hembeq" for homeomorphic embedding on
    lists. Added abbreviation "sublisteq" for special case
    "list_hembeq (op =)".

  - Theory Library/Sublist no longer provides "order" and "bot" type
    class instances for the prefix order (merely corresponding locale
    interpretations). The type class instances are now in theory
    Library/Prefix_Order.

  - The sublist relation of theory Library/Sublist_Order is now based
    on "Sublist.sublisteq".  Renamed lemmas accordingly:

      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
      le_list_append_mono ~> Sublist.list_hembeq_append_mono
      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
      le_list_drop_Cons ~> Sublist.sublisteq_Cons'
      le_list_drop_many ~> Sublist.sublisteq_drop_many
      le_list_filter_left ~> Sublist.sublisteq_filter_left
      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
      le_list_rev_take_iff ~> Sublist.sublisteq_append
      le_list_same_length ~> Sublist.sublisteq_same_length
      le_list_take_many_iff ~> Sublist.sublisteq_append'
      less_eq_list.drop ~> less_eq_list_drop
      less_eq_list.induct ~> less_eq_list_induct
      not_le_list_length ~> Sublist.not_sublisteq_length

INCOMPATIBILITY.

* New theory Library/Countable_Set.

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

* Theory Library/FuncSet: Extended support for Pi and extensional and
introduce the extensional dependent function space "PiE". Replaced
extensional_funcset by an abbreviation, and renamed lemmas from
extensional_funcset to PiE as follows:

  extensional_empty  ~>  PiE_empty
  extensional_funcset_empty_domain  ~>  PiE_empty_domain
  extensional_funcset_empty_range  ~>  PiE_empty_range
  extensional_funcset_arb  ~>  PiE_arb
  extensional_funcset_mem  ~>  PiE_mem
  extensional_funcset_extend_domainI  ~>  PiE_fun_upd
  extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE
  extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq
  card_extensional_funcset  ~>  card_PiE
  finite_extensional_funcset  ~>  finite_PiE

INCOMPATIBILITY.

* Theory Library/FinFun: theory of almost everywhere constant
functions (supersedes the AFP entry "Code Generation for Functions as
Data").

* Theory Library/Phantom: generic phantom type to make a type
parameter appear in a constant's type.  This alternative to adding
TYPE('a) as another parameter avoids unnecessary closures in generated
code.

* Theory Library/RBT_Impl: efficient construction of red-black trees
from sorted associative lists. Merging two trees with rbt_union may
return a structurally different tree than before.  Potential
INCOMPATIBILITY.

* Theory Library/IArray: immutable arrays with code generation.

* Theory Library/Finite_Lattice: theory of finite lattices.

* HOL/Multivariate_Analysis: replaced

  "basis :: 'a::euclidean_space => nat => real"
  "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"

on euclidean spaces by using the inner product "_ \<bullet> _" with
vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by
"SUM i : Basis. f i * r i".

  With this change the following constants are also changed or removed:

    DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)
    a $$ i  ~>  inner a i  (where i : Basis)
    cart_base i  removed
    \<pi>, \<pi>'  removed

  Theorems about these constants where removed.

  Renamed lemmas:

    component_le_norm  ~>  Basis_le_norm
    euclidean_eq  ~>  euclidean_eq_iff
    differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart
    euclidean_simps  ~>  inner_simps
    independent_basis  ~>  independent_Basis
    span_basis  ~>  span_Basis
    in_span_basis  ~>  in_span_Basis
    norm_bound_component_le  ~>  norm_boound_Basis_le
    norm_bound_component_lt  ~>  norm_boound_Basis_lt
    component_le_infnorm  ~>  Basis_le_infnorm

INCOMPATIBILITY.

* HOL/Probability:

  - Added simproc "measurable" to automatically prove measurability.

  - Added induction rules for sigma sets with disjoint union
    (sigma_sets_induct_disjoint) and for Borel-measurable functions
    (borel_measurable_induct).

  - Added the Daniell-Kolmogorov theorem (the existence the limit of a
    projective family).

* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the
AFP entry "Ordinals_and_Cardinals").

* HOL/BNF: New (co)datatype package based on bounded natural functors
with support for mixed, nested recursion and interesting non-free
datatypes.

* HOL/Finite_Set and Relation: added new set and relation operations
expressed by Finite_Set.fold.

* New theory HOL/Library/RBT_Set: implementation of sets by red-black
trees for the code generator.

* HOL/Library/RBT and HOL/Library/Mapping have been converted to
Lifting/Transfer.
possible INCOMPATIBILITY.

* HOL/Set: renamed Set.project -> Set.filter
INCOMPATIBILITY.


*** Document preparation ***

* Dropped legacy antiquotations "term_style" and "thm_style", since
styles may be given as arguments to "term" and "thm" already.
Discontinued legacy styles "prem1" .. "prem19".

* Default LaTeX rendering 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.


*** ML ***

* The default limit for maximum number of worker threads is now 8,
instead of 4, in correspondence to capabilities of contemporary
hardware and Poly/ML runtime system.

* Type Seq.results and related operations support embedded error
messages within lazy enumerations, and thus allow to provide
informative errors in the absence of any usable results.

* Renamed Position.str_of to Position.here to emphasize that this is a
formal device to inline positions into message text, but not
necessarily printing visible text.


*** 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.  The "isabelle mkroot" tool prepares
session root directories for use with "isabelle build", similar to
former "isabelle mkdir" for "isabelle usedir".  Note that this affects
document preparation as well.  INCOMPATIBILITY, isabelle usedir /
mkdir / make are rendered obsolete.

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

  isabelle build -s -b HOL

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

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

* The "isabelle logo" tool produces EPS and PDF format simultaneously.
Minor INCOMPATIBILITY in command-line options.

* The "isabelle install" tool has now a simpler command-line.  Minor
INCOMPATIBILITY.

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

* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general
platform family: "linux", "macos", "windows".

* The ML system is configured as regular component, and no longer
picked up from some surrounding directory.  Potential INCOMPATIBILITY
for home-made settings.

* Improved ML runtime statistics (heap, threads, future tasks etc.).

* 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