NEWS

 constants with qualified polymorphism (according to the class
 context).  Within the body context of a 'class' target, a separate
 syntax layer ("user space type system") takes care of converting
 between global polymorphic consts and internal locale representation.
 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).
+"isatool doc classes" provides a tutorial.
 
 * Yet another code generator framework allows to generate executable
 code for ML and Haskell (including Isabelle classes).  A short usage
 sketch:
 

     writing OCaml code to a file:
         code_gen <list of constants (term syntax)> in OCaml <filename>
     writing Haskell code to a bunch of files:
         code_gen <list of constants (term syntax)> in Haskell <filename>
 
-Reasonable default setup of framework in HOL/Main.
+    evaluating propositions to True/False using code generation:
+        method ``eval''
+
+Reasonable default setup of framework in HOL.
 
 Theorem attributs for selecting and transforming function equations theorems:
 
     [code fun]:        select a theorem as function equation for a specific constant
     [code fun del]:    deselect a theorem as function equation for a specific constant

 codegen".
 
 * Code generator: consts in 'consts_code' Isar commands are now
 referred to by usual term syntax (including optional type
 annotations).
-
-* Code generator: basic definitions (from 'definition', 'constdefs',
-or primitive 'instance' definitions) are added automatically to the
-table of defining equations.  Primitive defs are not used as defining
-equations by default any longer.  Defining equations are now definitly
-restricted to meta "==" and object equality "=".
 
 * Command 'no_translations' removes translation rules from theory
 syntax.
 
 * Overloaded definitions are now actually checked for acyclic

 background processes.  It generates calls to the "metis" method if
 successful. These can be pasted into the proof.  Users do not have to
 wait for the automatic provers to return.  WARNING: does not really
 work with multi-threading.
 
-* Localized monotonicity predicate in theory "Orderings"; integrated
-lemmas max_of_mono and min_of_mono with this predicate.
-INCOMPATIBILITY.
-
-* Class "div" now inherits from class "times" rather than "type".
-INCOMPATIBILITY.
-
 * New "auto_quickcheck" feature tests outermost goal statements for
 potential counter-examples.  Controlled by ML references
 auto_quickcheck (default true) and auto_quickcheck_time_limit (default
 5000 milliseconds).  Fails silently if statements is outside of
 executable fragment, or any other codgenerator problem occurs.
 
-* Internal reorganisation of `size' of datatypes: size theorems
-"foo.size" are no longer subsumed by "foo.simps" (but are still
-simplification rules by default!); theorems "prod.size" now named
-"*.size"
-
-* The transitivity reasoner for partial and linear orders is set up
-for locales "order" and "linorder" generated by the new class package
-(instead of axiomatic type classes used before).  Instances of the
-reasoner are available in all contexts importing or interpreting these
-locales.  Method "order" invokes the reasoner separately; the reasoner
-is also integrated with the Simplifier as a solver.  Diagnostic
-command 'print_orders' shows the available instances of the reasoner
-in the current context.
-
-* Formulation of theorem "dense" changed slightly due to integration
-with new class dense_linear_order.
-
-* HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice,
-Linorder etc.  have disappeared; operations defined in terms of
-fold_set now are named Inf_fin, Sup_fin.  INCOMPATIBILITY.
-
-* HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
-
-* HOL-Word: New extensive library and type for generic, fixed size
-machine words, with arithemtic, bit-wise, shifting and rotating
-operations, reflection into int, nat, and bool lists, automation for
-linear arithmetic (by automatic reflection into nat or int), including
-lemmas on overflow and monotonicity.  Instantiated to all appropriate
-arithmetic type classes, supporting automatic simplification of
-numerals on all operations.
-
-* Library/Boolean_Algebra: locales for abstract boolean algebras.
-
-* Library/Numeral_Type: numbers as types, e.g. TYPE(32).
-
-* Code generator library theories:
-  - Code_Integer represents HOL integers by big integer literals in target
-    languages.
-  - Code_Char represents HOL characters by character literals in target
-    languages.
-  - Code_Char_chr like Code_Char, but also offers treatment of character
-    codes; includes Code_Integer.
-  - Executable_Set allows to generate code for finite sets using lists.
-  - Executable_Rat implements rational numbers as triples (sign, enumerator,
-    denominator).
-  - Executable_Real implements a subset of real numbers, namly those
-    representable by rational numbers.
-  - Efficient_Nat implements natural numbers by integers, which in general will
-    result in higher efficency; pattern matching with 0/Suc is eliminated;
-    includes Code_Integer.
-  - Code_Index provides an additional datatype index which is mapped to
-    target-language built-in integers.
-  - Code_Message provides an additional datatype message_string} which is isomorphic to
-    strings; messages are mapped to target-language strings.
-
-* New package for inductive predicates
-
-  An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
-
-    inductive
-      p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
-      for z_1 :: U_1 and ... and z_n :: U_m
-    where
-      rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
-    | ...
-
-  with full support for type-inference, rather than
-
-    consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
-
-    abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
-    where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
-
-    inductive "s z_1 ... z_m"
-    intros
-      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
-      ...
-
-  For backward compatibility, there is a wrapper allowing inductive
-  sets to be defined with the new package via
-
-    inductive_set
-      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
-      for z_1 :: U_1 and ... and z_n :: U_m
-    where
-      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
-    | ...
-
-  or
-
-    inductive_set
-      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
-      and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
-      for z_1 :: U_1 and ... and z_n :: U_m
-    where
-      "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
-    | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
-    | ...
-
-  if the additional syntax "p ..." is required.
-
-  Numerous examples can be found in the subdirectories src/HOL/Auth,
-  src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava.
-
-  INCOMPATIBILITIES:
-
-  - Since declaration and definition of inductive sets or predicates
-    is no longer separated, abbreviations involving the newly
-    introduced sets or predicates must be specified together with the
-    introduction rules after the 'where' keyword (see above), rather
-    than before the actual inductive definition.
-
-  - The variables in induction and elimination rules are now
-    quantified in the order of their occurrence in the introduction
-    rules, rather than in alphabetical order. Since this may break
-    some proofs, these proofs either have to be repaired, e.g. by
-    reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case'
-    statements of the form
-
-      case (rule_i a_i_1 ... a_i_{k_i})
-
-    or the old order of quantification has to be restored by explicitly adding
-    meta-level quantifiers in the introduction rules, i.e.
-
-      | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
-
-  - The format of the elimination rules is now
-
-      p z_1 ... z_m x_1 ... x_n ==>
-        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
-        ==> ... ==> P
-
-    for predicates and
-
-      (x_1, ..., x_n) : s z_1 ... z_m ==>
-        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
-        ==> ... ==> P
-
-    for sets rather than
-
-      x : s z_1 ... z_m ==>
-        (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
-        ==> ... ==> P
-
-    This may require terms in goals to be expanded to n-tuples
-    (e.g. using case_tac or simplification with the split_paired_all
-    rule) before the above elimination rule is applicable.
-
-  - The elimination or case analysis rules for (mutually) inductive
-    sets or predicates are now called "p_1.cases" ... "p_k.cases". The
-    list of rules "p_1_..._p_k.elims" is no longer available.
-
-* Case-expressions allow arbitrary constructor-patterns (including
-"_") and take their order into account, like in functional
-programming.  Internally, this is translated into nested
-case-expressions; missing cases are added and mapped to the predefined
-constant "undefined". In complicated cases printing may no longer show
-the original input but the internal form. Lambda-abstractions allow
-the same form of pattern matching: "% pat1 => e1 | ..." is an
-abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new
-variable.
-
-* IntDef: The constant "int :: nat => int" has been removed; now "int"
-is an abbreviation for "of_nat :: nat => int". The simplification
-rules for "of_nat" have been changed to work like "int" did
-previously.  Potential INCOMPATIBILITY:
-  - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
-  - of_nat_diff and of_nat_mult are no longer default simp rules
-
-* Method "algebra" solves polynomial equations over (semi)rings using
-Groebner bases. The (semi)ring structure is defined by locales and the
-tool setup depends on that generic context. Installing the method for
-a specific type involves instantiating the locale and possibly adding
-declarations for computation on the coefficients.  The method is
-already instantiated for natural numbers and for the axiomatic class
-of idoms with numerals.  See also the paper by Chaieb and Wenzel at
-CALCULEMUS 2007 for the general principles underlying this
-architecture of context-aware proof-tools.
-
-* Method "ferrack" implements quantifier elimination over
-special-purpose dense linear orders using locales (analogous to
-"algebra"). The method is already installed for class
-{ordered_field,recpower,number_ring} which subsumes real, hyperreal,
-rat, etc.
-
-* Former constant "List.op @" now named "List.append".  Use ML
-antiquotations @{const_name List.append} or @{term " ... @ ... "} to
-circumvent possible incompatibilities when working on ML level.
+* New constant "undefined" with axiom "undefined x = undefined".
+
+* Added class "HOL.eq", allowing for code generation with polymorphic
+equality.
 
 * Some renaming of class constants due to canonical name prefixing in
 the new 'class' package:
 
-    HOL.abs ~> HOL.minus_class.abs
+    HOL.abs ~> HOL.abs_class.abs
     HOL.divide ~> HOL.divide_class.divide
+    0 ~> HOL.zero_class.zero
+    1 ~> HOL.one_class.one
+    op + ~> HOL.plus_class.plus
+    op - ~> HOL.minus_class.minus
+    uminus ~> HOL.minus_class.uminus
+    op * ~> HOL.times_class.times
+    op < ~> HOL.ord_class.less
+    op <= > HOL.ord_class.less_eq
     Nat.power ~> Power.power_class.power
     Nat.size ~> Nat.size_class.size
     Numeral.number_of ~> Numeral.number_class.number_of
     FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf
     FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup
     Orderings.min ~> Orderings.ord_class.min
     Orderings.max ~> Orderings.ord_class.max
-
-INCOMPATIBILITY.
+    Divides.op div ~> Divides.div_class.div
+    Divides.op mod ~> Divides.div_class.mod
+    Divides.op dvd ~> Divides.div_class.dvd
+
+INCOMPATIBILITY.  Adaptions may be required in the following cases:
+
+a) User-defined constants using any of the names "plus", "minus",
+"times", "less" or "less_eq". The standard syntax translations for
+"+", "-" and "*" may go wrong.  INCOMPATIBILITY: use more specific
+names.
+
+b) Variables named "plus", "minus", "times", "less", "less_eq"
+INCOMPATIBILITY: use more specific names.
+
+c) Permutative equations (e.g. "a + b = b + a")
+Since the change of names also changes the order of terms, permutative
+rewrite rules may get applied in a different order. Experience shows
+that this is rarely the case (only two adaptions in the whole Isabelle
+distribution).  INCOMPATIBILITY: rewrite proofs
+
+d) ML code directly refering to constant names
+This in general only affects hand-written proof tactics, simprocs and
+so on.  INCOMPATIBILITY: grep your sourcecode and replace names.
+Consider using @{const_name} antiquotation.
 
 * New class "default" with associated constant "default".
-
-* New constant "undefined" with axiom "undefined x = undefined".
-
-* primrec: missing cases mapped to "undefined" instead of "arbitrary".
-
-* New function listsum :: 'a list => 'a for arbitrary monoids.
-Special syntax: "SUM x <- xs. f x" (and latex variants)
-
-* New syntax for Haskell-like list comprehension (input only), eg.
-[(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy.
-
-* The special syntax for function "filter" has changed from [x :
-xs. P] to [x <- xs. P] to avoid an ambiguity caused by list
-comprehension syntax, and for uniformity.  INCOMPATIBILITY.
-
-* [a..b] is now defined for arbitrary linear orders.  It used to be
-defined on nat only, as an abbreviation for [a..<Suc b]
-INCOMPATIBILITY.
-
-* Renamed lemma "set_take_whileD"  to "set_takeWhileD".
-
-* New functions "sorted" and "sort" in src/HOL/List.thy.
 
 * Function "sgn" is now overloaded and available on int, real, complex
 (and other numeric types), using class "sgn".  Two possible defs of
 sgn are given as equational assumptions in the classes sgn_if and
 sgn_div_norm; ordered_idom now also inherits from sgn_if.
 INCOMPATIBILITY.
 
-* New lemma collection field_simps (an extension of ring_simps) for
-manipulating (in)equations involving division. Multiplies with all
-denominators that can be proved to be non-zero (in equations) or
-positive/negative (in inequations).
-
-* Lemma collections ring_eq_simps, group_eq_simps and ring_distrib
-have been improved and renamed to ring_simps, group_simps and
-ring_distribs.  Removed lemmas field_xyz in theory Ring_and_Field
-because they were subsumed by lemmas xyz.  INCOMPATIBILITY.
-
-* Theory Library/Commutative_Ring: switched from recdef to function
-package; constants add, mul, pow now curried.  Infix syntax for
-algebraic operations.
-
-* More uniform lattice theory development in HOL.
+* Locale "partial_order" now unified with class "order" (cf. theory
+Orderings), added parameter "less".  INCOMPATIBILITY.
+
+* Renamings in classes "order" and "linorder": facts "refl", "trans" and
+"cases" to "order_refl", "order_trans" and "linorder_cases", to avoid
+clashes with HOL "refl" and "trans".  INCOMPATIBILITY.
+
+* Classes "order" and "linorder": potential INCOMPATIBILITY due to
+changed order of proof goals in instance proofs.
+
+* The transitivity reasoner for partial and linear orders is set up
+for classes "order" and "linorder".  Instances of the reasoner are available
+in all contexts importing or interpreting the corresponding locales.
+Method "order" invokes the reasoner separately; the reasoner
+is also integrated with the Simplifier as a solver.  Diagnostic
+command 'print_orders' shows the available instances of the reasoner
+in the current context.
+
+* Localized monotonicity predicate in theory "Orderings"; integrated
+lemmas max_of_mono and min_of_mono with this predicate.
+INCOMPATIBILITY.
+
+* Formulation of theorem "dense" changed slightly due to integration
+with new class dense_linear_order.
+
+* Uniform lattice theory development in HOL.
 
     constants "meet" and "join" now named "inf" and "sup"
     constant "Meet" now named "Inf"
 
     classes "meet_semilorder" and "join_semilorder" now named

     listsp_meet_eq          ~> listsp_inf_eq
 
     meet_min                ~> inf_min
     join_max                ~> sup_max
 
-* Renamed classes "order" and "linorder": facts "refl", "trans" and
-"cases" to "order_refl", "order_trans" and "linorder_cases", to avoid
-clashes with HOL "refl" and "trans".  INCOMPATIBILITY.
-
-* Classes "order" and "linorder": potential INCOMPATIBILITY due to
-changed order of proof goals instance proofs.
-
-* Locale "partial_order" now unified with class "order" (cf. theory
-Orderings), added parameter "less".  INCOMPATIBILITY.
+* Added syntactic class "size"; overloaded constant "size" now has
+type "'a::size ==> bool"
+
+* Internal reorganisation of `size' of datatypes: size theorems
+"foo.size" are no longer subsumed by "foo.simps" (but are still
+simplification rules by default!); theorems "prod.size" now named
+"*.size".
+
+* Class "div" now inherits from class "times" rather than "type".
+INCOMPATIBILITY.
+
+* HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice,
+Linorder etc.  have disappeared; operations defined in terms of
+fold_set now are named Inf_fin, Sup_fin.  INCOMPATIBILITY.
+
+* HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
+
+* HOL-Word: New extensive library and type for generic, fixed size
+machine words, with arithemtic, bit-wise, shifting and rotating
+operations, reflection into int, nat, and bool lists, automation for
+linear arithmetic (by automatic reflection into nat or int), including
+lemmas on overflow and monotonicity.  Instantiated to all appropriate
+arithmetic type classes, supporting automatic simplification of
+numerals on all operations.
+
+* Library/Boolean_Algebra: locales for abstract boolean algebras.
+
+* Library/Numeral_Type: numbers as types, e.g. TYPE(32).
+
+* Code generator library theories:
+  - Code_Integer represents HOL integers by big integer literals in target
+    languages.
+  - Code_Char represents HOL characters by character literals in target
+    languages.
+  - Code_Char_chr like Code_Char, but also offers treatment of character
+    codes; includes Code_Integer.
+  - Executable_Set allows to generate code for finite sets using lists.
+  - Executable_Rat implements rational numbers as triples (sign, enumerator,
+    denominator).
+  - Executable_Real implements a subset of real numbers, namly those
+    representable by rational numbers.
+  - Efficient_Nat implements natural numbers by integers, which in general will
+    result in higher efficency; pattern matching with 0/Suc is eliminated;
+    includes Code_Integer.
+  - Code_Index provides an additional datatype index which is mapped to
+    target-language built-in integers.
+  - Code_Message provides an additional datatype message_string} which is isomorphic to
+    strings; messages are mapped to target-language strings.
+
+* New package for inductive predicates
+
+  An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
+
+    inductive
+      p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
+    | ...
+
+  with full support for type-inference, rather than
+
+    consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+
+    abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+    where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
+
+    inductive "s z_1 ... z_m"
+    intros
+      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
+      ...
+
+  For backward compatibility, there is a wrapper allowing inductive
+  sets to be defined with the new package via
+
+    inductive_set
+      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
+    | ...
+
+  or
+
+    inductive_set
+      s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
+      and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
+      for z_1 :: U_1 and ... and z_n :: U_m
+    where
+      "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
+    | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
+    | ...
+
+  if the additional syntax "p ..." is required.
+
+  Numerous examples can be found in the subdirectories src/HOL/Auth,
+  src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava.
+
+  INCOMPATIBILITIES:
+
+  - Since declaration and definition of inductive sets or predicates
+    is no longer separated, abbreviations involving the newly
+    introduced sets or predicates must be specified together with the
+    introduction rules after the 'where' keyword (see above), rather
+    than before the actual inductive definition.
+
+  - The variables in induction and elimination rules are now
+    quantified in the order of their occurrence in the introduction
+    rules, rather than in alphabetical order. Since this may break
+    some proofs, these proofs either have to be repaired, e.g. by
+    reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case'
+    statements of the form
+
+      case (rule_i a_i_1 ... a_i_{k_i})
+
+    or the old order of quantification has to be restored by explicitly adding
+    meta-level quantifiers in the introduction rules, i.e.
+
+      | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
+
+  - The format of the elimination rules is now
+
+      p z_1 ... z_m x_1 ... x_n ==>
+        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
+        ==> ... ==> P
+
+    for predicates and
+
+      (x_1, ..., x_n) : s z_1 ... z_m ==>
+        (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
+        ==> ... ==> P
+
+    for sets rather than
+
+      x : s z_1 ... z_m ==>
+        (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
+        ==> ... ==> P
+
+    This may require terms in goals to be expanded to n-tuples
+    (e.g. using case_tac or simplification with the split_paired_all
+    rule) before the above elimination rule is applicable.
+
+  - The elimination or case analysis rules for (mutually) inductive
+    sets or predicates are now called "p_1.cases" ... "p_k.cases". The
+    list of rules "p_1_..._p_k.elims" is no longer available.
+
+* Case-expressions allow arbitrary constructor-patterns (including
+"_") and take their order into account, like in functional
+programming.  Internally, this is translated into nested
+case-expressions; missing cases are added and mapped to the predefined
+constant "undefined". In complicated cases printing may no longer show
+the original input but the internal form. Lambda-abstractions allow
+the same form of pattern matching: "% pat1 => e1 | ..." is an
+abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new
+variable.
+
+* IntDef: The constant "int :: nat => int" has been removed; now "int"
+is an abbreviation for "of_nat :: nat => int". The simplification
+rules for "of_nat" have been changed to work like "int" did
+previously.  Potential INCOMPATIBILITY:
+  - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
+  - of_nat_diff and of_nat_mult are no longer default simp rules
+
+* Method "algebra" solves polynomial equations over (semi)rings using
+Groebner bases. The (semi)ring structure is defined by locales and the
+tool setup depends on that generic context. Installing the method for
+a specific type involves instantiating the locale and possibly adding
+declarations for computation on the coefficients.  The method is
+already instantiated for natural numbers and for the axiomatic class
+of idoms with numerals.  See also the paper by Chaieb and Wenzel at
+CALCULEMUS 2007 for the general principles underlying this
+architecture of context-aware proof-tools.
+
+* Method "ferrack" implements quantifier elimination over
+special-purpose dense linear orders using locales (analogous to
+"algebra"). The method is already installed for class
+{ordered_field,recpower,number_ring} which subsumes real, hyperreal,
+rat, etc.
+
+* Former constant "List.op @" now named "List.append".  Use ML
+antiquotations @{const_name List.append} or @{term " ... @ ... "} to
+circumvent possible incompatibilities when working on ML level.
+
+* primrec: missing cases mapped to "undefined" instead of "arbitrary".
+
+* New function listsum :: 'a list => 'a for arbitrary monoids.
+Special syntax: "SUM x <- xs. f x" (and latex variants)
+
+* New syntax for Haskell-like list comprehension (input only), eg.
+[(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy.
+
+* The special syntax for function "filter" has changed from [x :
+xs. P] to [x <- xs. P] to avoid an ambiguity caused by list
+comprehension syntax, and for uniformity.  INCOMPATIBILITY.
+
+* [a..b] is now defined for arbitrary linear orders.  It used to be
+defined on nat only, as an abbreviation for [a..<Suc b]
+INCOMPATIBILITY.
+
+* Renamed lemma "set_take_whileD"  to "set_takeWhileD".
+
+* New functions "sorted" and "sort" in src/HOL/List.thy.
+
+* New lemma collection field_simps (an extension of ring_simps) for
+manipulating (in)equations involving division. Multiplies with all
+denominators that can be proved to be non-zero (in equations) or
+positive/negative (in inequations).
+
+* Lemma collections ring_eq_simps, group_eq_simps and ring_distrib
+have been improved and renamed to ring_simps, group_simps and
+ring_distribs.  Removed lemmas field_xyz in theory Ring_and_Field
+because they were subsumed by lemmas xyz.  INCOMPATIBILITY.
+
+* Theory Library/Commutative_Ring: switched from recdef to function
+package; constants add, mul, pow now curried.  Infix syntax for
+algebraic operations.
 
 * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
 INCOMPATIBILITY.
 
 * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj.
 INCOMPATIBILITY.
-
-* Added syntactic class "size"; overloaded constant "size" now has
-type "'a::size ==> bool"
-
-* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
-dvd" to "Divides.div_class.div", "Divides.div_class.mod" and
-"Divides.dvd". INCOMPATIBILITY.
 
 * Method "lexicographic_order" automatically synthesizes termination
 relations as lexicographic combinations of size measures -- 'function'
 package.
 

 INCOMPATIBILITY: translations containing list_all2 may go wrong,
 better use 'abbreviation'.
 
 * Renamed constant "List.op mem" to "List.member".  INCOMPATIBILITY.
 
-* Renamed constants "0" to "HOL.zero_class.zero" and "1" to
-"HOL.one_class.one".  INCOMPATIBILITY.
-
-* Added class "HOL.eq", allowing for code generation with polymorphic
-equality.
-
 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has
 been abandoned in favour of plain 'int'.  INCOMPATIBILITY --
 significant changes for setting up numeral syntax for types:
   - New constants Numeral.pred and Numeral.succ instead
       of former Numeral.bin_pred and Numeral.bin_succ.

 further src/HOL/ex/NormalForm.thy and src/Tools/nbe.ML.
 
 * Alternative iff syntax "A <-> B" for equality on bool (with priority
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).
-
-* Renamed constants in HOL.thy and Orderings.thy:
-    op +   ~> HOL.plus_class.plus
-    op -   ~> HOL.minus_class.minus
-    uminus ~> HOL.minus_class.uminus
-    abs    ~> HOL.abs_class.abs
-    op *   ~> HOL.times_class.times
-    op <   ~> HOL.ord_class.less
-    op <=  ~> HOL.ord_class.less_eq
-
-Adaptions may be required in the following cases:
-
-a) User-defined constants using any of the names "plus", "minus",
-"times", "less" or "less_eq". The standard syntax translations for
-"+", "-" and "*" may go wrong.  INCOMPATIBILITY: use more specific
-names.
-
-b) Variables named "plus", "minus", "times", "less", "less_eq"
-INCOMPATIBILITY: use more specific names.
-
-c) Permutative equations (e.g. "a + b = b + a")
-Since the change of names also changes the order of terms, permutative
-rewrite rules may get applied in a different order. Experience shows
-that this is rarely the case (only two adaptions in the whole Isabelle
-distribution).  INCOMPATIBILITY: rewrite proofs
-
-d) ML code directly refering to constant names
-This in general only affects hand-written proof tactics, simprocs and
-so on.  INCOMPATIBILITY: grep your sourcecode and replace names.
-Consider using @{const_name} antiquotation.
 
 * Relations less (<) and less_eq (<=) are also available on type bool.
 Modified syntax to disallow nesting without explicit parentheses,
 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".  Potential
 INCOMPATIBILITY.