Isabelle NEWS -- history user-relevant changes

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

 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 (e.g. displayed as tooltips)

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

   - improved support for Unicode outside original 16bit range

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

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

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

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

 are now statically evaluated: the resulting theorem is stored instead

 of the original expression.  INCOMPATIBILITY in rare situations, where

 the historic accident of dynamic re-evaluation in interpretations

 etc. was exploited.

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

 declaration, and results are standardized before being stored.  Thus

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

 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of

 indices of schematic variables.

 * Renamed some inner syntax categories:

     num ~> num_token

     xnum ~> xnum_token

     xstr ~> str_token

 Minor INCOMPATIBILITY.  Note that in practice "num_const" or

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

 position information via constraints).

 * Simplified configuration options for syntax ambiguity: see

 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

 manual.  Minor INCOMPATIBILITY.

 * Forward declaration of outer syntax keywords within the theory

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

 commands to be used in the same theory where defined.

 *** Pure ***

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

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

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

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

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

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

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

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

 undocumented feature.)

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

 collection of foundational premises in the context (already marked as

 legacy since Isabelle2011).

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

 instead.  INCOMPATIBILITY.

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

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

 *** HOL ***

 * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").

 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",

 which has been removed. It supercedes "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.

 * Discontinued old Tutorial on Isar ("isar-overview");

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

 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.

 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and

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

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

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

 pruned from any tinkering with former theorems mem_def and Collect_def

 as far as possible.

 For developments which deliberately mixed predicates and sets, a

 planning step is necessary to determine what should become a predicate

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

 Isabelle2011-1 before jumping right into the current release.

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

 * Code generation by default implements sets as container type rather

 than predicates.  INCOMPATIBILITY.

 * New proof import from HOL Light: 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.

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

 * 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 ~> (dropped, use symp_def and sym_def instead)

   transp_def ~> transp_trans

   Domain_def ~> Domain_unfold

   Range_def ~> Domain_converse [symmetric]

 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

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

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

 INCOMPATIBILITY.

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

 * Concrete syntax for case expressions includes constraints for source

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

 INCOMPATIBILITY for old-style syntax translations that augment the

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

 one_case.

 * Discontinued configuration option "syntax_positions": atomic terms

 in parse trees are always annotated by position constraints.

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

 association lists with distinct keys.

 * 'datatype' specifications allow explicit sort constraints.

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

 use theory HOL/Library/Nat_Bijection instead.

 * 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

 * 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

 * New tactic "word_bitwise" for splitting machine word equalities and

 inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word

 session. Supports addition, subtraction, multiplication, shifting by

 constants, bitwise operators and numeric constants. Requires fixed-length word

 types, cannot operate on 'a word. Solves many standard word identies outright

 and converts more into first order problems amenable to blast or similar. See

 HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy.

 * Clarified attribute "mono_set": pure declaration without modifying

 the result of the fact expression.

 * "Transitive_Closure.ntrancl": bounded transitive closure on

 relations.

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

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

 INCOMPATIBILITY, use the corresponding generic theorems instead.

   zminus_zminus ~> minus_minus

   zminus_0 ~> minus_zero

   zminus_zadd_distrib ~> minus_add_distrib

   zadd_commute ~> add_commute

   zadd_assoc ~> add_assoc

   zadd_left_commute ~> add_left_commute

   zadd_ac ~> add_ac

   zmult_ac ~> mult_ac

   zadd_0 ~> add_0_left

   zadd_0_right ~> add_0_right

   zadd_zminus_inverse2 ~> left_minus

   zmult_zminus ~> mult_minus_left

   zmult_commute ~> mult_commute

   zmult_assoc ~> mult_assoc

   zadd_zmult_distrib ~> left_distrib

   zadd_zmult_distrib2 ~> right_distrib

   zdiff_zmult_distrib ~> left_diff_distrib

   zdiff_zmult_distrib2 ~> right_diff_distrib

   zmult_1 ~> mult_1_left

   zmult_1_right ~> mult_1_right

   zle_refl ~> order_refl

   zle_trans ~> order_trans

   zle_antisym ~> order_antisym

   zle_linear ~> linorder_linear

   zless_linear ~> linorder_less_linear

   zadd_left_mono ~> add_left_mono

   zadd_strict_right_mono ~> add_strict_right_mono

   zadd_zless_mono ~> add_less_le_mono

   int_0_less_1 ~> zero_less_one

   int_0_neq_1 ~> zero_neq_one

   zless_le ~> less_le

   zpower_zadd_distrib ~> power_add

   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

   zero_le_zpower_abs ~> zero_le_power_abs

 * Theory Deriv: Renamed

   DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

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

 case distinctions at the same time.  E.g.

   list.exhaust [case_product nat.exhaust]

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

 a list and a nat.

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

 * New Transfer 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 changes, 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.

 * New Lifting package:

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

   - Replaced remote E-SInE with remote Satallax in the default setup.

   - 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 "eventually_elim" method as a generalized variant of the

 eventually_elim* rules. Supports structured proofs.

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

 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar

 (not just JRE).

 * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name

 notation, which is useful for the jEdit file browser, for example.

 New in Isabelle2011-1 (October 2011)

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

 *** General ***

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

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

   - Management of multiple theory files directly from the editor

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

     files for checking).

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

     highlighting, tooltips and hyperlinks to jump to defining source

     positions.

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

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

     theory output and other non-Isabelle text boxes).

   - Refined scheduling of proof checking and printing of results,

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

     narrowing allows to restrict buffer perspectives explicitly.)

   - Reduced CPU performance requirements, usable on machines with few

     cores.

   - Reduced memory requirements due to pruning of unused document

     versions (garbage collection).

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

 including some remaining limitations.

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

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

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

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

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

 INCOMPATIBILITY.

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

 digests.  Discontinued former path/modtime identification and optional

 ISABELLE_FILE_IDENT plugin scripts.

 * Parallelization of nested Isar proofs is subject to

 Goal.parallel_proofs_threshold (default 100).  See also isabelle

 usedir option -Q.

 * Name space: former unsynchronized references are now proper

 configuration options, with more conventional names:

   long_names   ~> names_long

   short_names  ~> names_short

   unique_names ~> names_unique

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

   declare [[names_unique = false]]

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

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

 may have to be refined after enriching a proof context.

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

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

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

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

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

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

     "Classical Reasoner".

 *** HOL ***

 * Class bot and top require underlying partial order rather than

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

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

 generalized theorems INF_cong and SUP_cong.  New type classes for

 complete boolean algebras and complete linear orders.  Lemmas

 Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in

 class complete_linorder.

 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,

 Sup_fun_def, Inf_apply, Sup_apply.

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

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

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

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

   Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right

   Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right

   Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right

   Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right

   Inter_def ~> INF_def, image_def

   Union_def ~> SUP_def, image_def

   INT_eq ~> INF_def, and image_def

   UN_eq ~> SUP_def, and image_def

   INF_subset ~> INF_superset_mono [OF _ order_refl]

 More consistent and comprehensive names:

   INTER_eq_Inter_image ~> INF_def

   UNION_eq_Union_image ~> SUP_def

   INFI_def ~> INF_def

   SUPR_def ~> SUP_def

   INF_leI ~> INF_lower

   INF_leI2 ~> INF_lower2

   le_INFI ~> INF_greatest

   le_SUPI ~> SUP_upper

   le_SUPI2 ~> SUP_upper2

   SUP_leI ~> SUP_least

   INFI_bool_eq ~> INF_bool_eq

   SUPR_bool_eq ~> SUP_bool_eq

   INFI_apply ~> INF_apply

   SUPR_apply ~> SUP_apply

   INTER_def ~> INTER_eq

   UNION_def ~> UNION_eq

 INCOMPATIBILITY.

 * Renamed theory Complete_Lattice to Complete_Lattices.

 INCOMPATIBILITY.

 * Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,

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

 Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,

 Sup_insert are now declared as [simp].  INCOMPATIBILITY.

 * Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,

 compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,

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

 INCOMPATIBILITY.

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

 constants.  INCOMPATIBILITY: Changes in the argument order of the

 (mostly internal) locale predicates for some derived classes.

 * Theorem collections ball_simps and bex_simps do not contain theorems

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

 UN_ball_bex_simps.  INCOMPATIBILITY.

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

 separate type class floor_ceiling.

 * Theory Finite_Set: more coherent development of fold_set locales:

     locale fun_left_comm ~> locale comp_fun_commute

     locale fun_left_comm_idem ~> locale comp_fun_idem

 Both use point-free characterization; interpretation proofs may need

 adjustment.  INCOMPATIBILITY.

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

 accordance with standard mathematical terminology. INCOMPATIBILITY.

 * Theory Complex_Main: The locale interpretations for the

 bounded_linear and bounded_bilinear locales have been removed, in

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

 original names for distributivity theorems, potential INCOMPATIBILITY.

   divide.add ~> add_divide_distrib

   divide.diff ~> diff_divide_distrib

   divide.setsum ~> setsum_divide_distrib

   mult.add_right ~> right_distrib

   mult.diff_right ~> right_diff_distrib

   mult_right.setsum ~> setsum_right_distrib

   mult_left.diff ~> left_diff_distrib

 * Theory Complex_Main: Several redundant theorems have been removed or

 replaced by more general versions. INCOMPATIBILITY.

   real_diff_def ~> minus_real_def

   real_divide_def ~> divide_real_def

   real_less_def ~> less_le

   real_abs_def ~> abs_real_def

   real_sgn_def ~> sgn_real_def

   real_mult_commute ~> mult_commute

   real_mult_assoc ~> mult_assoc

   real_mult_1 ~> mult_1_left

   real_add_mult_distrib ~> left_distrib

   real_zero_not_eq_one ~> zero_neq_one

   real_mult_inverse_left ~> left_inverse

   INVERSE_ZERO ~> inverse_zero

   real_le_refl ~> order_refl

   real_le_antisym ~> order_antisym

   real_le_trans ~> order_trans

   real_le_linear ~> linear

   real_le_eq_diff ~> le_iff_diff_le_0

   real_add_left_mono ~> add_left_mono

   real_mult_order ~> mult_pos_pos

   real_mult_less_mono2 ~> mult_strict_left_mono

   real_of_int_real_of_nat ~> real_of_int_of_nat_eq

   real_0_le_divide_iff ~> zero_le_divide_iff

   realpow_two_disj ~> power2_eq_iff

   real_squared_diff_one_factored ~> square_diff_one_factored

   realpow_two_diff ~> square_diff_square_factored

   reals_complete2 ~> complete_real

   real_sum_squared_expand ~> power2_sum

   exp_ln_eq ~> ln_unique

   expi_add ~> exp_add

   expi_zero ~> exp_zero

   lemma_DERIV_subst ~> DERIV_cong

   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

   LIMSEQ_const ~> tendsto_const

   LIMSEQ_norm ~> tendsto_norm

   LIMSEQ_add ~> tendsto_add

   LIMSEQ_minus ~> tendsto_minus

   LIMSEQ_minus_cancel ~> tendsto_minus_cancel

   LIMSEQ_diff ~> tendsto_diff

   bounded_linear.LIMSEQ ~> bounded_linear.tendsto

   bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

   LIMSEQ_mult ~> tendsto_mult

   LIMSEQ_inverse ~> tendsto_inverse

   LIMSEQ_divide ~> tendsto_divide

   LIMSEQ_pow ~> tendsto_power

   LIMSEQ_setsum ~> tendsto_setsum

   LIMSEQ_setprod ~> tendsto_setprod

   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

   LIMSEQ_imp_rabs ~> tendsto_rabs

   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

   LIMSEQ_Complex ~> tendsto_Complex

   LIM_ident ~> tendsto_ident_at

   LIM_const ~> tendsto_const

   LIM_add ~> tendsto_add

   LIM_add_zero ~> tendsto_add_zero

   LIM_minus ~> tendsto_minus

   LIM_diff ~> tendsto_diff

   LIM_norm ~> tendsto_norm

   LIM_norm_zero ~> tendsto_norm_zero

   LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

   LIM_norm_zero_iff ~> tendsto_norm_zero_iff

   LIM_rabs ~> tendsto_rabs

   LIM_rabs_zero ~> tendsto_rabs_zero

   LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

   LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

   LIM_compose ~> tendsto_compose

   LIM_mult ~> tendsto_mult

   LIM_scaleR ~> tendsto_scaleR

   LIM_of_real ~> tendsto_of_real

   LIM_power ~> tendsto_power

   LIM_inverse ~> tendsto_inverse

   LIM_sgn ~> tendsto_sgn

   isCont_LIM_compose ~> isCont_tendsto_compose

   bounded_linear.LIM ~> bounded_linear.tendsto

   bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

   bounded_bilinear.LIM ~> bounded_bilinear.tendsto

   bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

   bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

   bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

   LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

 * Theory Complex_Main: The definition of infinite series was

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

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

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

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

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

 * Code generation:

   - Theory Library/Code_Char_ord provides native ordering of

     characters in the target language.

   - Commands code_module and code_library are legacy, use export_code

     instead.

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

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

     reactivated by the following theory command:

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

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

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

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

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

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

 syntax.

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

 still available as a legacy feature for some time.

 * Nitpick:

   - Added "need" and "total_consts" options.

   - Reintroduced "show_skolems" option by popular demand.

   - Renamed attribute: nitpick_def ~> nitpick_unfold.

     INCOMPATIBILITY.

 * Sledgehammer:

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

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

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

   - Automatically preplay and minimize proofs before showing them if

     this can be done within reasonable time.

   - sledgehammer available_provers ~> sledgehammer supported_provers.

     INCOMPATIBILITY.

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

     "max_mono_iters", and "max_new_mono_instances" options.

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

     Types" Proof General menu item. INCOMPATIBILITY.

 * Metis:

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

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

     INCOMPATIBILITY.

 * Command 'try':

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

     "elim:" options. INCOMPATIBILITY.

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

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

 * Quickcheck:

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

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

   - Added post-processing of terms to obtain readable counterexamples

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

   - New counterexample generator quickcheck[narrowing] enables

     narrowing-based testing.  Requires the Glasgow Haskell compiler

     with its installation location defined in the Isabelle settings

     environment as ISABELLE_GHC.

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

     (formly in HOL/Library).

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

 use 'partial_function' instead.

 * Theory Library/Extended_Reals replaces now the positive extended

 reals found in probability theory. This file is extended by

 Multivariate_Analysis/Extended_Real_Limits.

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

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

 INCOMPATIBILITY.

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

 been moved here.  INCOMPATIBILITY.

 * Theory Library/Saturated provides type of numbers with saturated

 arithmetic.

 * Theory Library/Product_Lattice defines a pointwise ordering for the

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

 and lattice type classes.

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

 method for proving "countable" class instances for datatypes.

 * Theory Library/Cset_Monad allows do notation for computable sets

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

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

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

 abstract type. INCOMPATIBILITY.

   - RBT is split into RBT and RBT_Mapping.

   - AssocList is split and renamed into AList and AList_Mapping.

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

   - Cset is split into Cset and List_Cset.

 * Theory Library/Nat_Infinity has been renamed to

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

 constants:

   type inat   ~> type enat

   Fin         ~> enat

   Infty       ~> infinity (overloaded)

   iSuc        ~> eSuc

   the_Fin     ~> the_enat

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

 been renamed accordingly. INCOMPATIBILITY.

 * Session Multivariate_Analysis: The euclidean_space type class now

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

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

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

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

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

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

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

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

 changed to match. Definition theorems for overloaded constants now use

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

 been renamed as follows (INCOMPATIBILITY):

   Cart_eq          ~> vec_eq_iff

   dist_nth_le_cart ~> dist_vec_nth_le

   tendsto_vector   ~> vec_tendstoI

   Cauchy_vector    ~> vec_CauchyI

 * Session Multivariate_Analysis: Several duplicate theorems have been

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

 general versions. INCOMPATIBILITY.

   finite_choice ~> finite_set_choice

   eventually_conjI ~> eventually_conj

   eventually_and ~> eventually_conj_iff

   eventually_false ~> eventually_False

   setsum_norm ~> norm_setsum

   Lim_sequentially ~> LIMSEQ_def

   Lim_ident_at ~> LIM_ident

   Lim_const ~> tendsto_const

   Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

   Lim_neg ~> tendsto_minus

   Lim_add ~> tendsto_add

   Lim_sub ~> tendsto_diff

   Lim_mul ~> tendsto_scaleR

   Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

   Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

   Lim_linear ~> bounded_linear.tendsto

   Lim_component ~> tendsto_euclidean_component

   Lim_component_cart ~> tendsto_vec_nth

   Lim_inner ~> tendsto_inner [OF tendsto_const]

   dot_lsum ~> inner_setsum_left

   dot_rsum ~> inner_setsum_right

   continuous_cmul ~> continuous_scaleR [OF continuous_const]

   continuous_neg ~> continuous_minus

   continuous_sub ~> continuous_diff

   continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

   continuous_mul ~> continuous_scaleR

   continuous_inv ~> continuous_inverse

   continuous_at_within_inv ~> continuous_at_within_inverse

   continuous_at_inv ~> continuous_at_inverse

   continuous_at_norm ~> continuous_norm [OF continuous_at_id]

   continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

   continuous_at_component ~> continuous_component [OF continuous_at_id]

   continuous_on_neg ~> continuous_on_minus

   continuous_on_sub ~> continuous_on_diff

   continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

   continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

   continuous_on_mul ~> continuous_on_scaleR

   continuous_on_mul_real ~> continuous_on_mult

   continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

   continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

   continuous_on_inverse ~> continuous_on_inv

   uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

   uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

   subset_interior ~> interior_mono

   subset_closure ~> closure_mono

   closure_univ ~> closure_UNIV

   real_arch_lt ~> reals_Archimedean2

   real_arch ~> reals_Archimedean3

   real_abs_norm ~> abs_norm_cancel

   real_abs_sub_norm ~> norm_triangle_ineq3

   norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

 * Session HOL-Probability:

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

   - Infinite products of probability measures are now available.

   - Sigma closure is independent, if the generator is independent

   - Use extended reals instead of positive extended

     reals. INCOMPATIBILITY.

 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

   expand_fun_below ~> fun_below_iff

   below_fun_ext ~> fun_belowI

   expand_cfun_eq ~> cfun_eq_iff

   ext_cfun ~> cfun_eqI

   expand_cfun_below ~> cfun_below_iff

   below_cfun_ext ~> cfun_belowI

   monofun_fun_fun ~> fun_belowD

   monofun_fun_arg ~> monofunE

   monofun_lub_fun ~> adm_monofun [THEN admD]

   cont_lub_fun ~> adm_cont [THEN admD]

   cont2cont_Rep_CFun ~> cont2cont_APP

   cont_Rep_CFun_app ~> cont_APP_app

   cont_Rep_CFun_app_app ~> cont_APP_app_app

   cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]

   cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]

   contlub_cfun ~> lub_APP [symmetric]

   contlub_LAM ~> lub_LAM [symmetric]

   thelubI ~> lub_eqI

   UU_I ~> bottomI

   lift_distinct1 ~> lift.distinct(1)

   lift_distinct2 ~> lift.distinct(2)

   Def_not_UU ~> lift.distinct(2)

   Def_inject ~> lift.inject

   below_UU_iff ~> below_bottom_iff

   eq_UU_iff ~> eq_bottom_iff

 *** Document preparation ***

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

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

 same.

 * Antiquotation @{value} evaluates the given term and presents its

 result.

 * Antiquotations: term style "isub" provides ad-hoc conversion of

 variables x1, y23 into subscripted form x\<^isub>1,

 y\<^isub>2\<^isub>3.

 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>

 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).

 * Localized \isabellestyle switch can be used within blocks or groups

 like this:

   \isabellestyle{it}  %preferred default

   {\isabellestylett @{text "typewriter stuff"}}

 * Discontinued special treatment of hard tabulators.  Implicit

 tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual

 layouts.

 *** ML ***

 * The inner syntax of sort/type/term/prop supports inlined YXML

 representations within quoted string tokens.  By encoding logical

 entities via Term_XML (in ML or Scala) concrete syntax can be

 bypassed, which is particularly useful for producing bits of text

 under external program control.

 * Antiquotations for ML and document preparation are managed as theory

 data, which requires explicit setup.

 * Isabelle_Process.is_active allows tools to check if the official

 process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop

 (better known as Proof General).

 * Structure Proof_Context follows standard naming scheme.  Old

 ProofContext is still available for some time as legacy alias.

 * Structure Timing provides various operations for timing; supersedes

 former start_timing/end_timing etc.

 * Path.print is the official way to show file-system paths to users

 (including quotes etc.).

 * Inner syntax: identifiers in parse trees of generic categories

 "logic", "aprop", "idt" etc. carry position information (disguised as

 type constraints).  Occasional INCOMPATIBILITY with non-compliant

 translations that choke on unexpected type constraints.  Positions can

 be stripped in ML translations via Syntax.strip_positions /

 Syntax.strip_positions_ast, or via the syntax constant

 "_strip_positions" within parse trees.  As last resort, positions can

 be disabled via the configuration option Syntax.positions, which is

 called "syntax_positions" in Isar attribute syntax.

 * Discontinued special status of various ML structures that contribute

 to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less

 pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,

 refer directly to Ast.Constant, Lexicon.is_identifier,

 Syntax_Trans.mk_binder_tr etc.

 * Typed print translation: discontinued show_sorts argument, which is

 already available via context of "advanced" translation.

 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic

 goal states; body tactic needs to address all subgoals uniformly.

 * Slightly more special eq_list/eq_set, with shortcut involving

 pointer equality (assumes that eq relation is reflexive).

 * Classical tactics use proper Proof.context instead of historic types

 claset/clasimpset.  Old-style declarations like addIs, addEs, addDs

 operate directly on Proof.context.  Raw type claset retains its use as

 snapshot of the classical context, which can be recovered via

 (put_claset HOL_cs) etc.  Type clasimpset has been discontinued.

 INCOMPATIBILITY, classical tactics and derived proof methods require

 proper Proof.context.

 *** System ***

 * Discontinued support for Poly/ML 5.2, which was the last version

 without proper multithreading and TimeLimit implementation.

 * Discontinued old lib/scripts/polyml-platform, which has been

 obsolete since Isabelle2009-2.

 * Various optional external tools are referenced more robustly and

 uniformly by explicit Isabelle settings as follows:

   ISABELLE_CSDP   (formerly CSDP_EXE)

   ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)

   ISABELLE_OCAML  (formerly EXEC_OCAML)

   ISABELLE_SWIPL  (formerly EXEC_SWIPL)

   ISABELLE_YAP    (formerly EXEC_YAP)

 Note that automated detection from the file-system or search path has

 been discontinued.  INCOMPATIBILITY.

 * Scala layer provides JVM method invocation service for static

 methods of type (String)String, see Invoke_Scala.method in ML.  For

 example:

   Invoke_Scala.method "java.lang.System.getProperty" "java.home"

 Together with YXML.string_of_body/parse_body and XML.Encode/Decode

 this allows to pass structured values between ML and Scala.

 * The IsabelleText fonts includes some further glyphs to support the

 Prover IDE.  Potential INCOMPATIBILITY: users who happen to have

 installed a local copy (which is normally *not* required) need to

 delete or update it from ~~/lib/fonts/.

 New in Isabelle2011 (January 2011)

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

 *** General ***

 * Experimental Prover IDE based on Isabelle/Scala and jEdit (see

 src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with

 useful tooltips and hyperlinks produced from its static analysis.  The

 bundled component provides an executable Isabelle tool that can be run

 like this:

   Isabelle2011/bin/isabelle jedit

 * Significantly improved Isabelle/Isar implementation manual.

 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

 (and thus refers to something like $HOME/.isabelle/Isabelle2011),

 while the default heap location within that directory lacks that extra

 suffix.  This isolates multiple Isabelle installations from each

 other, avoiding problems with old settings in new versions.

 INCOMPATIBILITY, need to copy/upgrade old user settings manually.

 * Source files are always encoded as UTF-8, instead of old-fashioned

 ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require

 the following package declarations:

   \usepackage[utf8]{inputenc}

   \usepackage{textcomp}

 * Explicit treatment of UTF-8 sequences as Isabelle symbols, such that

 a Unicode character is treated as a single symbol, not a sequence of

 non-ASCII bytes as before.  Since Isabelle/ML string literals may

 contain symbols without further backslash escapes, Unicode can now be

 used here as well.  Recall that Symbol.explode in ML provides a

 consistent view on symbols, while raw explode (or String.explode)

 merely give a byte-oriented representation.

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

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

 The global load path is still partially available as legacy feature.

 Minor INCOMPATIBILITY due to subtle change in file lookup: use

 explicit paths, relatively to the theory.

 * Special treatment of ML file names has been discontinued.

 Historically, optional extensions .ML or .sml were added on demand --

 at the cost of clarity of file dependencies.  Recall that Isabelle/ML

 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.

 * Various options that affect pretty printing etc. are now properly

 handled within the context via configuration options, instead of

 unsynchronized references or print modes.  There are both ML Config.T

 entities and Isar declaration attributes to access these.

   ML (Config.T)                 Isar (attribute)

   eta_contract                  eta_contract

   show_brackets                 show_brackets

   show_sorts                    show_sorts

   show_types                    show_types

   show_question_marks           show_question_marks

   show_consts                   show_consts

   show_abbrevs                  show_abbrevs

   Syntax.ast_trace              syntax_ast_trace

   Syntax.ast_stat               syntax_ast_stat

   Syntax.ambiguity_level        syntax_ambiguity_level

   Goal_Display.goals_limit      goals_limit

   Goal_Display.show_main_goal   show_main_goal

   Method.rule_trace             rule_trace

   Thy_Output.display            thy_output_display

   Thy_Output.quotes             thy_output_quotes

   Thy_Output.indent             thy_output_indent

   Thy_Output.source             thy_output_source

   Thy_Output.break              thy_output_break

 Note that corresponding "..._default" references in ML may only be

 changed globally at the ROOT session setup, but *not* within a theory.

 The option "show_abbrevs" supersedes the former print mode

 "no_abbrevs" with inverted meaning.

 * More systematic naming of some configuration options.

 INCOMPATIBILITY.

   trace_simp  ~>  simp_trace

   debug_simp  ~>  simp_debug

 * Support for real valued configuration options, using simplistic

 floating-point notation that coincides with the inner syntax for

 float_token.

 * Support for real valued preferences (with approximative PGIP type):

 front-ends need to accept "pgint" values in float notation.

 INCOMPATIBILITY.

 * The IsabelleText font now includes Cyrillic, Hebrew, Arabic from

 DejaVu Sans.

 * Discontinued support for Poly/ML 5.0 and 5.1 versions.

 *** Pure ***

 * Command 'type_synonym' (with single argument) replaces somewhat

 outdated 'types', which is still available as legacy feature for some

 time.

 * Command 'nonterminal' (with 'and' separated list of arguments)

 replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.

 * Command 'notepad' replaces former 'example_proof' for

 experimentation in Isar without any result.  INCOMPATIBILITY.

 * Locale interpretation commands 'interpret' and 'sublocale' accept

 lists of equations to map definitions in a locale to appropriate

 entities in the context of the interpretation.  The 'interpretation'

 command already provided this functionality.

 * Diagnostic command 'print_dependencies' prints the locale instances

 that would be activated if the specified expression was interpreted in

 the current context.  Variant "print_dependencies!" assumes a context

 without interpretations.

 * Diagnostic command 'print_interps' prints interpretations in proofs

 in addition to interpretations in theories.

 * Discontinued obsolete 'global' and 'local' commands to manipulate

 the theory name space.  Rare INCOMPATIBILITY.  The ML functions

 Sign.root_path and Sign.local_path may be applied directly where this

 feature is still required for historical reasons.

 * Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use

 'definition' instead.

 * The "prems" fact, which refers to the accidental collection of

 foundational premises in the context, is now explicitly marked as

 legacy feature and will be discontinued soon.  Consider using "assms"

 of the head statement or reference facts by explicit names.

 * Document antiquotations @{class} and @{type} print classes and type

 constructors.

 * Document antiquotation @{file} checks file/directory entries within

 the local file system.

 *** HOL ***

 * Coercive subtyping: functions can be declared as coercions and type

 inference will add them as necessary upon input of a term.  Theory

 Complex_Main declares real :: nat => real and real :: int => real as

 coercions. A coercion function f is declared like this:

   declare [[coercion f]]

 To lift coercions through type constructors (e.g. from nat => real to

 nat list => real list), map functions can be declared, e.g.

   declare [[coercion_map map]]

 Currently coercion inference is activated only in theories including

 real numbers, i.e. descendants of Complex_Main.  This is controlled by

 the configuration option "coercion_enabled", e.g. it can be enabled in

 other theories like this:

   declare [[coercion_enabled]]

 * Command 'partial_function' provides basic support for recursive

 function definitions over complete partial orders.  Concrete instances

 are provided for i) the option type, ii) tail recursion on arbitrary

 types, and iii) the heap monad of Imperative_HOL.  See

 src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy

 for examples.

 * Function package: f.psimps rules are no longer implicitly declared

 as [simp].  INCOMPATIBILITY.

 * Datatype package: theorems generated for executable equality (class

 "eq") carry proper names and are treated as default code equations.

 * Inductive package: now offers command 'inductive_simps' to

 automatically derive instantiated and simplified equations for

 inductive predicates, similar to 'inductive_cases'.

 * Command 'enriched_type' allows to register properties of the

 functorial structure of types.

 * Improved infrastructure for term evaluation using code generator

 techniques, in particular static evaluation conversions.

 * Code generator: Scala (2.8 or higher) has been added to the target

 languages.

 * Code generator: globbing constant expressions "*" and "Theory.*"

 have been replaced by the more idiomatic "_" and "Theory._".

 INCOMPATIBILITY.

 * Code generator: export_code without explicit file declaration prints

 to standard output.  INCOMPATIBILITY.

 * Code generator: do not print function definitions for case

 combinators any longer.

 * Code generator: simplification with rules determined with

 src/Tools/Code/code_simp.ML and method "code_simp".

 * Code generator for records: more idiomatic representation of record

 types.  Warning: records are not covered by ancient SML code

 generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable

 rep_datatype declaration helps to succeed then:

   record 'a foo = ...

   ...

   rep_datatype foo_ext ...

 * Records: logical foundation type for records does not carry a

 '_type' suffix any longer (obsolete due to authentic syntax).

 INCOMPATIBILITY.

 * Quickcheck now by default uses exhaustive testing instead of random

 testing.  Random testing can be invoked by "quickcheck [random]",

 exhaustive testing by "quickcheck [exhaustive]".

 * Quickcheck instantiates polymorphic types with small finite

 datatypes by default. This enables a simple execution mechanism to

 handle quantifiers and function equality over the finite datatypes.

 * Quickcheck random generator has been renamed from "code" to

 "random".  INCOMPATIBILITY.

 * Quickcheck now has a configurable time limit which is set to 30

 seconds by default. This can be changed by adding [timeout = n] to the

 quickcheck command. The time limit for Auto Quickcheck is still set

 independently.

 * Quickcheck in locales considers interpretations of that locale for

 counter example search.

 * Sledgehammer:

   - Added "smt" and "remote_smt" provers based on the "smt" proof

     method. See the Sledgehammer manual for details ("isabelle doc

     sledgehammer").

   - Renamed commands:

     sledgehammer atp_info ~> sledgehammer running_provers

     sledgehammer atp_kill ~> sledgehammer kill_provers

     sledgehammer available_atps ~> sledgehammer available_provers

     INCOMPATIBILITY.

   - Renamed options:

     sledgehammer [atps = ...] ~> sledgehammer [provers = ...]

     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]

     sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]

     (and "ms" and "min" are no longer supported)

     INCOMPATIBILITY.

 * Nitpick:

   - Renamed options:

     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]

     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]

     INCOMPATIBILITY.

   - Added support for partial quotient types.

   - Added local versions of the "Nitpick.register_xxx" functions.

   - Added "whack" option.

   - Allow registration of quotient types as codatatypes.

   - Improved "merge_type_vars" option to merge more types.

   - Removed unsound "fast_descrs" option.

   - Added custom symmetry breaking for datatypes, making it possible to reach

     higher cardinalities.

   - Prevent the expansion of too large definitions.

 * Proof methods "metis" and "meson" now have configuration options

 "meson_trace", "metis_trace", and "metis_verbose" that can be enabled

 to diagnose these tools. E.g.

     using [[metis_trace = true]]

 * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available

 manually as command 'solve_direct'.

 * The default SMT solver Z3 must be enabled explicitly (due to

 licensing issues) by setting the environment variable

 Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For

 commercial applications, the SMT solver CVC3 is provided as fall-back;

 changing the SMT solver is done via the configuration option

 "smt_solver".

 * Remote SMT solvers need to be referred to by the "remote_" prefix,

 i.e. "remote_cvc3" and "remote_z3".

 * Added basic SMT support for datatypes, records, and typedefs using

 the oracle mode (no proofs).  Direct support of pairs has been dropped

 in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT

 support for a similar behavior).  Minor INCOMPATIBILITY.

 * Changed SMT configuration options:

   - Renamed:

     z3_proofs ~> smt_oracle (with inverted meaning)

     z3_trace_assms ~> smt_trace_used_facts

     INCOMPATIBILITY.

   - Added:

     smt_verbose

     smt_random_seed

     smt_datatypes

     smt_infer_triggers

     smt_monomorph_limit

     cvc3_options

     remote_cvc3_options

     remote_z3_options

     yices_options

 * Boogie output files (.b2i files) need to be declared in the theory

 header.

 * Simplification procedure "list_to_set_comprehension" rewrites list

 comprehensions applied to List.set to set comprehensions.  Occasional

 INCOMPATIBILITY, may be deactivated like this:

   declare [[simproc del: list_to_set_comprehension]]

 * Removed old version of primrec package.  INCOMPATIBILITY.

 * Removed simplifier congruence rule of "prod_case", as has for long

 been the case with "split".  INCOMPATIBILITY.

 * String.literal is a type, but not a datatype.  INCOMPATIBILITY.

 * Removed [split_format ... and ... and ...] version of

 [split_format].  Potential INCOMPATIBILITY.

 * Predicate "sorted" now defined inductively, with nice induction

 rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.

 * Constant "contents" renamed to "the_elem", to free the generic name

 contents for other uses.  INCOMPATIBILITY.

 * Renamed class eq and constant eq (for code generation) to class

 equal and constant equal, plus renaming of related facts and various

 tuning.  INCOMPATIBILITY.

 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

 * Removed output syntax "'a ~=> 'b" for "'a => 'b option".

 INCOMPATIBILITY.

 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to

 avoid confusion with finite sets.  INCOMPATIBILITY.

 * Abandoned locales equiv, congruent and congruent2 for equivalence

 relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same

 for congruent(2)).

 * Some previously unqualified names have been qualified:

   types

     bool ~> HOL.bool

     nat ~> Nat.nat

   constants

     Trueprop ~> HOL.Trueprop

     True ~> HOL.True

     False ~> HOL.False

     op & ~> HOL.conj

     op | ~> HOL.disj

     op --> ~> HOL.implies

     op = ~> HOL.eq

     Not ~> HOL.Not

     The ~> HOL.The

     All ~> HOL.All

     Ex ~> HOL.Ex

     Ex1 ~> HOL.Ex1

     Let ~> HOL.Let

     If ~> HOL.If

     Ball ~> Set.Ball

     Bex ~> Set.Bex

     Suc ~> Nat.Suc

     Pair ~> Product_Type.Pair

     fst ~> Product_Type.fst

     snd ~> Product_Type.snd

     curry ~> Product_Type.curry

     op : ~> Set.member

     Collect ~> Set.Collect

 INCOMPATIBILITY.

 * More canonical naming convention for some fundamental definitions:

     bot_bool_eq ~> bot_bool_def

     top_bool_eq ~> top_bool_def

     inf_bool_eq ~> inf_bool_def

     sup_bool_eq ~> sup_bool_def

     bot_fun_eq  ~> bot_fun_def

     top_fun_eq  ~> top_fun_def

     inf_fun_eq  ~> inf_fun_def

     sup_fun_eq  ~> sup_fun_def

 INCOMPATIBILITY.

 * More stylized fact names:

   expand_fun_eq ~> fun_eq_iff

   expand_set_eq ~> set_eq_iff

   set_ext       ~> set_eqI

   nat_number    ~> eval_nat_numeral

 INCOMPATIBILITY.

 * Refactoring of code-generation specific operations in theory List:

   constants

     null ~> List.null

   facts

     mem_iff ~> member_def

     null_empty ~> null_def

 INCOMPATIBILITY.  Note that these were not supposed to be used

 regularly unless for striking reasons; their main purpose was code

 generation.

 Various operations from the Haskell prelude are used for generating

 Haskell code.

 * Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV".  Term

 "surj f" is now an abbreviation of "range f = UNIV".  The theorems

 bij_def and surj_def are unchanged.  INCOMPATIBILITY.

 * Abolished some non-alphabetic type names: "prod" and "sum" replace

 "*" and "+" respectively.  INCOMPATIBILITY.

 * Name "Plus" of disjoint sum operator "<+>" is now hidden.  Write

 "Sum_Type.Plus" instead.

 * Constant "split" has been merged with constant "prod_case"; names of

 ML functions, facts etc. involving split have been retained so far,

 though.  INCOMPATIBILITY.

 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"

 instead.  INCOMPATIBILITY.

 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".

 INCOMPATIBILITY.

 * Former theory Library/Enum is now part of the HOL-Main image.

 INCOMPATIBILITY: all constants of the Enum theory now have to be

 referred to by its qualified name.

   enum    ~>  Enum.enum

   nlists  ~>  Enum.nlists

   product ~>  Enum.product

 * Theory Library/Monad_Syntax provides do-syntax for monad types.

 Syntax in Library/State_Monad has been changed to avoid ambiguities.

 INCOMPATIBILITY.

 * Theory Library/SetsAndFunctions has been split into

 Library/Function_Algebras and Library/Set_Algebras; canonical names

 for instance definitions for functions; various improvements.

 INCOMPATIBILITY.

 * Theory Library/Multiset provides stable quicksort implementation of

 sort_key.

 * Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.

 INCOMPATIBILITY.

 * Session Multivariate_Analysis: introduced a type class for euclidean

 space.  Most theorems are now stated in terms of euclidean spaces

 instead of finite cartesian products.

   types

     real ^ 'n ~>  'a::real_vector

               ~>  'a::euclidean_space

               ~>  'a::ordered_euclidean_space

         (depends on your needs)

   constants

      _ $ _        ~> _ $$ _

      \<chi> x. _  ~> \<chi>\<chi> x. _

      CARD('n)     ~> DIM('a)

 Also note that the indices are now natural numbers and not from some

 finite type. Finite cartesian products of euclidean spaces, products

 of euclidean spaces the real and complex numbers are instantiated to

 be euclidean_spaces.  INCOMPATIBILITY.

 * Session Probability: introduced pextreal as positive extended real

 numbers.  Use pextreal as value for measures.  Introduce the

 Radon-Nikodym derivative, product spaces and Fubini's theorem for

 arbitrary sigma finite measures.  Introduces Lebesgue measure based on

 the integral in Multivariate Analysis.  INCOMPATIBILITY.

 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.

 INCOMPATIBILITY.

 * Session SPARK (with image HOL-SPARK) provides commands to load and

 prove verification conditions generated by the SPARK Ada program

 verifier.  See also src/HOL/SPARK and src/HOL/SPARK/Examples.

 *** HOL-Algebra ***

 * Theorems for additive ring operations (locale abelian_monoid and

 descendants) are generated by interpretation from their multiplicative

 counterparts.  Names (in particular theorem names) have the mandatory

 qualifier 'add'.  Previous theorem names are redeclared for

 compatibility.

 * Structure "int_ring" is now an abbreviation (previously a

 definition).  This fits more natural with advanced interpretations.

 *** HOLCF ***

 * The domain package now runs in definitional mode by default: The

 former command 'new_domain' is now called 'domain'.  To use the domain

 package in its original axiomatic mode, use 'domain (unsafe)'.

 INCOMPATIBILITY.

 * The new class "domain" is now the default sort.  Class "predomain"

 is an unpointed version of "domain". Theories can be updated by

 replacing sort annotations as shown below.  INCOMPATIBILITY.

   'a::type ~> 'a::countable

   'a::cpo  ~> 'a::predomain

   'a::pcpo ~> 'a::domain

 * The old type class "rep" has been superseded by class "domain".

 Accordingly, users of the definitional package must remove any

 "default_sort rep" declarations.  INCOMPATIBILITY.

 * The domain package (definitional mode) now supports unpointed

 predomain argument types, as long as they are marked 'lazy'. (Strict

 arguments must be in class "domain".) For example, the following

 domain definition now works:

   domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")

 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class

 instances for types from main HOL: bool, nat, int, char, 'a + 'b,

 'a option, and 'a list.  Additionally, it configures fixrec and the

 domain package to work with these types.  For example:

   fixrec isInl :: "('a + 'b) u -> tr"

     where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"

   domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")

 * The "(permissive)" option of fixrec has been replaced with a

 per-equation "(unchecked)" option. See

 src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.

 * The "bifinite" class no longer fixes a constant "approx"; the class

 now just asserts that such a function exists.  INCOMPATIBILITY.

 * Former type "alg_defl" has been renamed to "defl".  HOLCF no longer

 defines an embedding of type 'a defl into udom by default; instances

 of "bifinite" and "domain" classes are available in

 src/HOL/HOLCF/Library/Defl_Bifinite.thy.

 * The syntax "REP('a)" has been replaced with "DEFL('a)".

 * The predicate "directed" has been removed.  INCOMPATIBILITY.

 * The type class "finite_po" has been removed.  INCOMPATIBILITY.

 * The function "cprod_map" has been renamed to "prod_map".

 INCOMPATIBILITY.

 * The monadic bind operator on each powerdomain has new binder syntax

 similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents

 "upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".

 * The infix syntax for binary union on each powerdomain has changed

 from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set

 syntax.  INCOMPATIBILITY.

 * The constant "UU" has been renamed to "bottom".  The syntax "UU" is

 still supported as an input translation.

 * Renamed some theorems (the original names are also still available).

   expand_fun_below   ~> fun_below_iff

   below_fun_ext      ~> fun_belowI

   expand_cfun_eq     ~> cfun_eq_iff

   ext_cfun           ~> cfun_eqI

   expand_cfun_below  ~> cfun_below_iff

   below_cfun_ext     ~> cfun_belowI

   cont2cont_Rep_CFun ~> cont2cont_APP

 * The Abs and Rep functions for various types have changed names.

 Related theorem names have also changed to match. INCOMPATIBILITY.

   Rep_CFun  ~> Rep_cfun

   Abs_CFun  ~> Abs_cfun

   Rep_Sprod ~> Rep_sprod

   Abs_Sprod ~> Abs_sprod

   Rep_Ssum  ~> Rep_ssum

   Abs_Ssum  ~> Abs_ssum

 * Lemmas with names of the form *_defined_iff or *_strict_iff have

 been renamed to *_bottom_iff.  INCOMPATIBILITY.

 * Various changes to bisimulation/coinduction with domain package:

   - Definitions of "bisim" constants no longer mention definedness.

   - With mutual recursion, "bisim" predicate is now curried.

   - With mutual recursion, each type gets a separate coind theorem.

   - Variable names in bisim_def and coinduct rules have changed.

 INCOMPATIBILITY.

 * Case combinators generated by the domain package for type "foo" are

 now named "foo_case" instead of "foo_when".  INCOMPATIBILITY.

 * Several theorems have been renamed to more accurately reflect the

 names of constants and types involved.  INCOMPATIBILITY.

   thelub_const    ~> lub_const

   lub_const       ~> is_lub_const

   thelubI         ~> lub_eqI

   is_lub_lub      ~> is_lubD2

   lubI            ~> is_lub_lub

   unique_lub      ~> is_lub_unique

   is_ub_lub       ~> is_lub_rangeD1

   lub_bin_chain   ~> is_lub_bin_chain

   lub_fun         ~> is_lub_fun

   thelub_fun      ~> lub_fun

   thelub_cfun     ~> lub_cfun

   thelub_Pair     ~> lub_Pair

   lub_cprod       ~> is_lub_prod

   thelub_cprod    ~> lub_prod

   minimal_cprod   ~> minimal_prod

   inst_cprod_pcpo ~> inst_prod_pcpo

   UU_I            ~> bottomI

   compact_UU      ~> compact_bottom

   deflation_UU    ~> deflation_bottom

   finite_deflation_UU ~> finite_deflation_bottom

 * Many legacy theorem names have been discontinued.  INCOMPATIBILITY.

   sq_ord_less_eq_trans ~> below_eq_trans

   sq_ord_eq_less_trans ~> eq_below_trans

   refl_less            ~> below_refl

   trans_less           ~> below_trans

   antisym_less         ~> below_antisym

   antisym_less_inverse ~> po_eq_conv [THEN iffD1]

   box_less             ~> box_below

   rev_trans_less       ~> rev_below_trans

   not_less2not_eq      ~> not_below2not_eq

   less_UU_iff          ~> below_UU_iff

   flat_less_iff        ~> flat_below_iff

   adm_less             ~> adm_below

   adm_not_less         ~> adm_not_below

   adm_compact_not_less ~> adm_compact_not_below

   less_fun_def         ~> below_fun_def

   expand_fun_less      ~> fun_below_iff

   less_fun_ext         ~> fun_belowI

   less_discr_def       ~> below_discr_def

   discr_less_eq        ~> discr_below_eq

   less_unit_def        ~> below_unit_def

   less_cprod_def       ~> below_prod_def

   prod_lessI           ~> prod_belowI

   Pair_less_iff        ~> Pair_below_iff

   fst_less_iff         ~> fst_below_iff

   snd_less_iff         ~> snd_below_iff

   expand_cfun_less     ~> cfun_below_iff

   less_cfun_ext        ~> cfun_belowI

   injection_less       ~> injection_below

   less_up_def          ~> below_up_def

   not_Iup_less         ~> not_Iup_below

   Iup_less             ~> Iup_below

   up_less              ~> up_below

   Def_inject_less_eq   ~> Def_below_Def

   Def_less_is_eq       ~> Def_below_iff

   spair_less_iff       ~> spair_below_iff

   less_sprod           ~> below_sprod

   spair_less           ~> spair_below

   sfst_less_iff        ~> sfst_below_iff

   ssnd_less_iff        ~> ssnd_below_iff

   fix_least_less       ~> fix_least_below

   dist_less_one        ~> dist_below_one

   less_ONE             ~> below_ONE

   ONE_less_iff         ~> ONE_below_iff

   less_sinlD           ~> below_sinlD

   less_sinrD           ~> below_sinrD

 *** FOL and ZF ***

 * All constant names are now qualified internally and use proper

 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.

 *** ML ***

 * Antiquotation @{assert} inlines a function bool -> unit that raises

 Fail if the argument is false.  Due to inlining the source position of

 failed assertions is included in the error output.

 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML

 text is in practice always evaluated with a stable theory checkpoint.

 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.

 * Antiquotation @{theory A} refers to theory A from the ancestry of

 the current context, not any accidental theory loader state as before.

 Potential INCOMPATIBILITY, subtle change in semantics.

 * Syntax.pretty_priority (default 0) configures the required priority

 of pretty-printed output and thus affects insertion of parentheses.

 * Syntax.default_root (default "any") configures the inner syntax

 category (nonterminal symbol) for parsing of terms.

 * Former exception Library.UnequalLengths now coincides with

 ListPair.UnequalLengths.

 * Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the

 main functionality is provided by structure Simplifier.

 * Renamed raw "explode" function to "raw_explode" to emphasize its

 meaning.  Note that internally to Isabelle, Symbol.explode is used in

 almost all situations.

 * Discontinued obsolete function sys_error and exception SYS_ERROR.

 See implementation manual for further details on exceptions in

 Isabelle/ML.

 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its

 meaning.

 * Renamed structure PureThy to Pure_Thy and moved most of its

 operations to structure Global_Theory, to emphasize that this is

 rarely-used global-only stuff.

 * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln

 instead (or tracing for high-volume output).

 * Configuration option show_question_marks only affects regular pretty

 printing of types and terms, not raw Term.string_of_vname.

 * ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare

 INCOMPATIBILITY, superseded by static antiquotations @{thm} and

 @{thms} for most purposes.

 * ML structure Unsynchronized is never opened, not even in Isar

 interaction mode as before.  Old Unsynchronized.set etc. have been

 discontinued -- use plain := instead.  This should be *rare* anyway,

 since modern tools always work via official context data, notably

 configuration options.

 * Parallel and asynchronous execution requires special care concerning

 interrupts.  Structure Exn provides some convenience functions that

 avoid working directly with raw Interrupt.  User code must not absorb

 interrupts -- intermediate handling (for cleanup etc.) needs to be

 followed by re-raising of the original exception.  Another common

 source of mistakes are "handle _" patterns, which make the meaning of

 the program subject to physical effects of the environment.

 New in Isabelle2009-2 (June 2010)

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

 *** General ***

 * Authentic syntax for *all* logical entities (type classes, type

 constructors, term constants): provides simple and robust

 correspondence between formal entities and concrete syntax.  Within

 the parse tree / AST representations, "constants" are decorated by

 their category (class, type, const) and spelled out explicitly with

 their full internal name.

 Substantial INCOMPATIBILITY concerning low-level syntax declarations

 and translations (translation rules and translation functions in ML).

 Some hints on upgrading:

   - Many existing uses of 'syntax' and 'translations' can be replaced

     by more modern 'type_notation', 'notation' and 'abbreviation',

     which are independent of this issue.

   - 'translations' require markup within the AST; the term syntax

     provides the following special forms:

       CONST c   -- produces syntax version of constant c from context

       XCONST c  -- literally c, checked as constant from context

       c         -- literally c, if declared by 'syntax'

     Plain identifiers are treated as AST variables -- occasionally the

     system indicates accidental variables via the error "rhs contains

     extra variables".

     Type classes and type constructors are marked according to their

     concrete syntax.  Some old translations rules need to be written

     for the "type" category, using type constructor application

     instead of pseudo-term application of the default category

     "logic".

   - 'parse_translation' etc. in ML may use the following

     antiquotations:

       @{class_syntax c}   -- type class c within parse tree / AST

       @{term_syntax c}    -- type constructor c within parse tree / AST

       @{const_syntax c}   -- ML version of "CONST c" above

       @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)

   - Literal types within 'typed_print_translations', i.e. those *not*

     represented as pseudo-terms are represented verbatim.  Use @{class

     c} or @{type_name c} here instead of the above syntax

     antiquotations.

 Note that old non-authentic syntax was based on unqualified base

 names, so all of the above "constant" names would coincide.  Recall

 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to

 diagnose syntax problems.

 * Type constructors admit general mixfix syntax, not just infix.

 * Concrete syntax may be attached to local entities without a proof

 body, too.  This works via regular mixfix annotations for 'fix',

 'def', 'obtain' etc. or via the explicit 'write' command, which is

 similar to the 'notation' command in theory specifications.

 * Discontinued unnamed infix syntax (legacy feature for many years) --

 need to specify constant name and syntax separately.  Internal ML

 datatype constructors have been renamed from InfixName to Infix etc.

 Minor INCOMPATIBILITY.

 * Schematic theorem statements need to be explicitly markup as such,

 via commands 'schematic_lemma', 'schematic_theorem',

 'schematic_corollary'.  Thus the relevance of the proof is made

 syntactically clear, which impacts performance in a parallel or

 asynchronous interactive environment.  Minor INCOMPATIBILITY.

 * Use of cumulative prems via "!" in some proof methods has been

 discontinued (old legacy feature).

 * References 'trace_simp' and 'debug_simp' have been replaced by

 configuration options stored in the context. Enabling tracing (the

 case of debugging is similar) in proofs works via

   using [[trace_simp = true]]

 Tracing is then active for all invocations of the simplifier in

 subsequent goal refinement steps. Tracing may also still be enabled or

 disabled via the ProofGeneral settings menu.

 * Separate commands 'hide_class', 'hide_type', 'hide_const',

 'hide_fact' replace the former 'hide' KIND command.  Minor

 INCOMPATIBILITY.

 * Improved parallelism of proof term normalization: usedir -p2 -q0 is

 more efficient than combinations with -q1 or -q2.

 *** Pure ***

 * Proofterms record type-class reasoning explicitly, using the

 "unconstrain" operation internally.  This eliminates all sort

 constraints from a theorem and proof, introducing explicit

 OFCLASS-premises.  On the proof term level, this operation is

 automatically applied at theorem boundaries, such that closed proofs

 are always free of sort constraints.  INCOMPATIBILITY for tools that

 inspect proof terms.

 * Local theory specifications may depend on extra type variables that

 are not present in the result type -- arguments TYPE('a) :: 'a itself

 are added internally.  For example:

   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"

 * Predicates of locales introduced by classes carry a mandatory

 "class" prefix.  INCOMPATIBILITY.

 * Vacuous class specifications observe default sort.  INCOMPATIBILITY.

 * Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use

 'class' instead.

 * Command 'code_reflect' allows to incorporate generated ML code into

 runtime environment; replaces immature code_datatype antiquotation.

 INCOMPATIBILITY.

 * Code generator: simple concept for abstract datatypes obeying

 invariants.

 * Code generator: details of internal data cache have no impact on the

 user space functionality any longer.

 * Methods "unfold_locales" and "intro_locales" ignore non-locale

 subgoals.  This is more appropriate for interpretations with 'where'.

 INCOMPATIBILITY.

 * Command 'example_proof' opens an empty proof body.  This allows to

 experiment with Isar, without producing any persistent result.

 * Commands 'type_notation' and 'no_type_notation' declare type syntax

 within a local theory context, with explicit checking of the

 constructors involved (in contrast to the raw 'syntax' versions).

 * Commands 'types' and 'typedecl' now work within a local theory

 context -- without introducing dependencies on parameters or

 assumptions, which is not possible in Isabelle/Pure.

 * Command 'defaultsort' has been renamed to 'default_sort', it works

 within a local theory context.  Minor INCOMPATIBILITY.

 *** HOL ***

 * Command 'typedef' now works within a local theory context -- without

 introducing dependencies on parameters or assumptions, which is not

 possible in Isabelle/Pure/HOL.  Note that the logical environment may

 contain multiple interpretations of local typedefs (with different

 non-emptiness proofs), even in a global theory context.

 * New package for quotient types.  Commands 'quotient_type' and

 'quotient_definition' may be used for defining types and constants by

 quotient constructions.  An example is the type of integers created by

 quotienting pairs of natural numbers:

   fun

     intrel :: "(nat * nat) => (nat * nat) => bool"

   where

     "intrel (x, y) (u, v) = (x + v = u + y)"

   quotient_type int = "nat * nat" / intrel

     by (auto simp add: equivp_def expand_fun_eq)

   quotient_definition

     "0::int" is "(0::nat, 0::nat)"

 The method "lifting" can be used to lift of theorems from the

 underlying "raw" type to the quotient type.  The example

 src/HOL/Quotient_Examples/FSet.thy includes such a quotient

 construction and provides a reasoning infrastructure for finite sets.

 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid

 clash with new theory Quotient in Main HOL.

 * Moved the SMT binding into the main HOL session, eliminating

 separate HOL-SMT session.

 * List membership infix mem operation is only an input abbreviation.

 INCOMPATIBILITY.

 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy

 for future developements; former Library/Word.thy is still present in

 the AFP entry RSAPPS.

 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no

 longer shadowed.  INCOMPATIBILITY.

 * Dropped theorem duplicate comp_arith; use semiring_norm instead.

 INCOMPATIBILITY.

 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.

 INCOMPATIBILITY.

 * Dropped normalizing_semiring etc; use the facts in semiring classes

 instead.  INCOMPATIBILITY.

 * Dropped several real-specific versions of lemmas about floor and

 ceiling; use the generic lemmas from theory "Archimedean_Field"

 instead.  INCOMPATIBILITY.

   floor_number_of_eq         ~> floor_number_of

   le_floor_eq_number_of      ~> number_of_le_floor

   le_floor_eq_zero           ~> zero_le_floor

   le_floor_eq_one            ~> one_le_floor

   floor_less_eq_number_of    ~> floor_less_number_of

   floor_less_eq_zero         ~> floor_less_zero

   floor_less_eq_one          ~> floor_less_one

   less_floor_eq_number_of    ~> number_of_less_floor

   less_floor_eq_zero         ~> zero_less_floor

   less_floor_eq_one          ~> one_less_floor

   floor_le_eq_number_of      ~> floor_le_number_of

   floor_le_eq_zero           ~> floor_le_zero

   floor_le_eq_one            ~> floor_le_one

   floor_subtract_number_of   ~> floor_diff_number_of

   floor_subtract_one         ~> floor_diff_one

   ceiling_number_of_eq       ~> ceiling_number_of

   ceiling_le_eq_number_of    ~> ceiling_le_number_of

   ceiling_le_zero_eq         ~> ceiling_le_zero

   ceiling_le_eq_one          ~> ceiling_le_one

   less_ceiling_eq_number_of  ~> number_of_less_ceiling

   less_ceiling_eq_zero       ~> zero_less_ceiling

   less_ceiling_eq_one        ~> one_less_ceiling

   ceiling_less_eq_number_of  ~> ceiling_less_number_of

   ceiling_less_eq_zero       ~> ceiling_less_zero

   ceiling_less_eq_one        ~> ceiling_less_one

   le_ceiling_eq_number_of    ~> number_of_le_ceiling

   le_ceiling_eq_zero         ~> zero_le_ceiling

   le_ceiling_eq_one          ~> one_le_ceiling

   ceiling_subtract_number_of ~> ceiling_diff_number_of

   ceiling_subtract_one       ~> ceiling_diff_one

 * Theory "Finite_Set": various folding_XXX locales facilitate the

 application of the various fold combinators on finite sets.

 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"

 provides abstract red-black tree type which is backed by "RBT_Impl" as

 implementation.  INCOMPATIBILTY.

 * Theory Library/Coinductive_List has been removed -- superseded by

 AFP/thys/Coinductive.

 * Theory PReal, including the type "preal" and related operations, has

 been removed.  INCOMPATIBILITY.

 * Real: new development using Cauchy Sequences.

 * Split off theory "Big_Operators" containing setsum, setprod,

 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

 * Theory "Rational" renamed to "Rat", for consistency with "Nat",

 "Int" etc.  INCOMPATIBILITY.

 * Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.

 * New set of rules "ac_simps" provides combined assoc / commute

 rewrites for all interpretations of the appropriate generic locales.

 * Renamed theory "OrderedGroup" to "Groups" and split theory

 "Ring_and_Field" into theories "Rings" and "Fields"; for more

 appropriate and more consistent names suitable for name prefixes

 within the HOL theories.  INCOMPATIBILITY.

 * Some generic constants have been put to appropriate theories:

   - less_eq, less: Orderings

   - zero, one, plus, minus, uminus, times, abs, sgn: Groups

   - inverse, divide: Rings

 INCOMPATIBILITY.

 * More consistent naming of type classes involving orderings (and

 lattices):

     lower_semilattice                   ~> semilattice_inf

     upper_semilattice                   ~> semilattice_sup

     dense_linear_order                  ~> dense_linorder

     pordered_ab_group_add               ~> ordered_ab_group_add

     pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs

     pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add

     pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le

     pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add

     pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring

     pordered_cancel_semiring            ~> ordered_cancel_semiring

     pordered_comm_monoid_add            ~> ordered_comm_monoid_add

     pordered_comm_ring                  ~> ordered_comm_ring

     pordered_comm_semiring              ~> ordered_comm_semiring

     pordered_ring                       ~> ordered_ring

     pordered_ring_abs                   ~> ordered_ring_abs

     pordered_semiring                   ~> ordered_semiring

     ordered_ab_group_add                ~> linordered_ab_group_add

     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add

     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add

     ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict

     ordered_field                       ~> linordered_field

     ordered_field_no_lb                 ~> linordered_field_no_lb

     ordered_field_no_ub                 ~> linordered_field_no_ub

     ordered_field_dense_linear_order    ~> dense_linordered_field

     ordered_idom                        ~> linordered_idom

     ordered_ring                        ~> linordered_ring

     ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor

     ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor

     ordered_ring_strict                 ~> linordered_ring_strict

     ordered_semidom                     ~> linordered_semidom

     ordered_semiring                    ~> linordered_semiring

     ordered_semiring_1                  ~> linordered_semiring_1

     ordered_semiring_1_strict           ~> linordered_semiring_1_strict

     ordered_semiring_strict             ~> linordered_semiring_strict

   The following slightly odd type classes have been moved to a

   separate theory Library/Lattice_Algebras:

     lordered_ab_group_add               ~> lattice_ab_group_add

     lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs

     lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add

     lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add

     lordered_ring                       ~> lattice_ring

 INCOMPATIBILITY.

 * Refined field classes:

   - classes division_ring_inverse_zero, field_inverse_zero,

     linordered_field_inverse_zero include rule inverse 0 = 0 --

     subsumes former division_by_zero class;

   - numerous lemmas have been ported from field to division_ring.

 INCOMPATIBILITY.

 * Refined algebra theorem collections:

   - dropped theorem group group_simps, use algebra_simps instead;

   - dropped theorem group ring_simps, use field_simps instead;

   - proper theorem collection field_simps subsumes former theorem

     groups field_eq_simps and field_simps;

   - dropped lemma eq_minus_self_iff which is a duplicate for

     equal_neg_zero.

 INCOMPATIBILITY.

 * Theory Finite_Set and List: some lemmas have been generalized from

 sets to lattices:

   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf

   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup

   inter_Inter_fold_inter        ~> inf_Inf_fold_inf

   union_Union_fold_union        ~> sup_Sup_fold_sup

   Inter_fold_inter              ~> Inf_fold_inf

   Union_fold_union              ~> Sup_fold_sup

   inter_INTER_fold_inter        ~> inf_INFI_fold_inf

   union_UNION_fold_union        ~> sup_SUPR_fold_sup

   INTER_fold_inter              ~> INFI_fold_inf

   UNION_fold_union              ~> SUPR_fold_sup

 * Theory "Complete_Lattice": lemmas top_def and bot_def have been

 replaced by the more convenient lemmas Inf_empty and Sup_empty.

 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed

 by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace

 former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right

 subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.

 * Reorganized theory Multiset: swapped notation of pointwise and

 multiset order:

   - pointwise ordering is instance of class order with standard syntax

     <= and <;

   - multiset ordering has syntax <=# and <#; partial order properties

     are provided by means of interpretation with prefix

     multiset_order;

   - less duplication, less historical organization of sections,

     conversion from associations lists to multisets, rudimentary code

     generation;

   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,

     if needed.

 Renamed:

   multiset_eq_conv_count_eq  ~>  multiset_ext_iff

   multi_count_ext  ~>  multiset_ext

   diff_union_inverse2  ~>  diff_union_cancelR

 INCOMPATIBILITY.

 * Theory Permutation: replaced local "remove" by List.remove1.

 * Code generation: ML and OCaml code is decorated with signatures.

 * Theory List: added transpose.

 * Library/Nat_Bijection.thy is a collection of bijective functions

 between nat and other types, which supersedes the older libraries

 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.