configuration options stored in the context. Enabling tracing

 configuration options stored in the context. Enabling tracing (the

 (the case of debugging is similar) in proofs works via

 case of debugging is similar) in proofs works via

   using [[trace_simp=true]]

   using [[trace_simp = true]]

 Tracing is then active for all invocations of the simplifier

 Tracing is then active for all invocations of the simplifier in

 in subsequent goal refinement steps. Tracing may also still be

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

 enabled or disabled via the ProofGeneral settings menu.

 disabled via the ProofGeneral settings menu.

 * Predicates of locales introduces by classes carry a mandatory "class"

 * Predicates of locales introduces by classes carry a mandatory

 prefix.  INCOMPATIBILITY.

 "class" prefix.  INCOMPATIBILITY.

 * 'code_reflect' allows to incorporate generated ML code into

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

 runtime environment;  replaces immature code_datatype antiquotation.

 runtime environment; replaces immature code_datatype antiquotation.

 * Old 'axclass' has been discontinued.  Use 'class' instead.  INCOMPATIBILITY.

 * Old 'axclass' command has been discontinued.  Use 'class' instead.

 INCOMPATIBILITY.

 * Code generator: simple concept for abstract datatypes obeying invariants.

 * Code generator: simple concept for abstract datatypes obeying

 invariants.

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

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

 the user space functionality any longer.

 user space functionality any longer.

 * Methods unfold_locales and intro_locales ignore non-locale subgoals.  This

 * Methods unfold_locales and intro_locales ignore non-locale subgoals.

 is more appropriate for interpretations with 'where'.  INCOMPATIBILITY.

 This is more appropriate for interpretations with 'where'.

 INCOMPATIBILITY.

 * Command 'defaultsort' is renamed to 'default_sort', it works within

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

 a local theory context.  Minor INCOMPATIBILITY.

 within a local theory context.  Minor INCOMPATIBILITY.

 order of type variables. INCOMPATIBILITY: Tools working with proof

 order of type variables. Potential INCOMPATIBILITY for tools working

 terms may need to be adapted.

 with proof terms.

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

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

 no longer shadowed.  INCOMPATIBILITY.

 longer shadowed.  INCOMPATIBILITY.

 * Dropped normalizing_semiring etc; use the facts in semiring classes instead.

 * Dropped normalizing_semiring etc; use the facts in semiring classes

 INCOMPATIBILITY.

 instead.  INCOMPATIBILITY.

 * Theory 'Finite_Set': various folding_* locales facilitate the application

 * Theory 'Finite_Set': various folding_XXX locales facilitate the

 of the various fold combinators on finite sets.

 application of the various fold combinators on finite sets.

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

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

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

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

 as implementation.  INCOMPATIBILTY.

 implementation.  INCOMPATIBILTY.

 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,

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

 Min, Max from theory Finite_Set.  INCOMPATIBILITY.

 Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

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

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

 "Int" etc.  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

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

 * More consistent naming of type classes involving orderings (and

 for all interpretations of the appropriate generic locales.

 lattices):

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

   The following slightly odd type classes have been moved to

   The following slightly odd type classes have been moved to a

   a separate theory Library/Lattice_Algebras.thy:

   separate theory Library/Lattice_Algebras.thy:

   * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero

   - classes division_ring_inverse_zero, field_inverse_zero,

     include rule inverse 0 = 0 -- subsumes former division_by_zero class.

     linordered_field_inverse_zero include rule inverse 0 = 0 --

   * numerous lemmas have been ported from field to division_ring;

     subsumes former division_by_zero class;

   INCOMPATIBILITY.

   - numerous lemmas have been ported from field to division_ring.

 INCOMPATIBILITY.

   * dropped theorem group group_simps, use algebra_simps instead;

   - dropped theorem group group_simps, use algebra_simps instead;

   * dropped theorem group ring_simps, use field_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;

   - proper theorem collection field_simps subsumes former theorem

   * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.

     groups field_eq_simps and field_simps;

   INCOMPATIBILITY.

   - dropped lemma eq_minus_self_iff which is a duplicate for

     equal_neg_zero.

 INCOMPATIBILITY.

 * Reorganized theory Multiset: swapped notation of pointwise and multiset order:

 * Reorganized theory Multiset: swapped notation of pointwise and

   * pointwise ordering is instance of class order with standard syntax <= and <;

 multiset order:

   * multiset ordering has syntax <=# and <#; partial order properties are provided

   - pointwise ordering is instance of class order with standard syntax

       by means of interpretation with prefix multiset_order;

     <= and <;

   * less duplication, less historical organization of sections,

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

       conversion from associations lists to multisets, rudimentary code generation;

     are provided by means of interpretation with prefix

   * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.

     multiset_order;

   INCOMPATIBILITY.

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

 INCOMPATIBILITY.