1.1 --- a/NEWS	Thu Feb 28 15:54:37 2008 +0100
     1.2 +++ b/NEWS	Thu Feb 28 15:55:04 2008 +0100
     1.3 @@ -29,56 +29,62 @@
     1.4  instance operations together with an instantiation proof.
     1.5  Type-checking phase allows to refer to class operations uniformly.
     1.6  See HOL/Complex/Complex.thy for an Isar example and
     1.7 -HOL/Library/Eval.thy for an ML example.  Supersedes previous
     1.8 -experimental versions.
     1.9 +HOL/Library/Eval.thy for an ML example.
    1.10  
    1.11  
    1.12  *** HOL ***
    1.13  
    1.14 -* Theory Int: The representation of numerals has changed.  The infix operator
    1.15 -BIT and the bit datatype with constructors B0 and B1 have disappeared.
    1.16 -INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
    1.17 -and "y BIT bit.B1", respectively.  Theorems involving BIT, B0, or B1 have been
    1.18 -renamed with "Bit0" or "Bit1" accordingly.
    1.19 -
    1.20 -* Theory Nat: definition of <= and < on natural numbers no longer depend
    1.21 -on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
    1.22 -have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
    1.23 -and less_eq [symmetric] instead.
    1.24 -
    1.25 -* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin (whose purpose 
    1.26 -mainly is for various fold_set functionals) have been abandoned in favour of
    1.27 -the existing algebraic classes ab_semigroup_mult, comm_monoid_mult,
    1.28 -ab_semigroup_idem_mult, lower_semilattice (resp. upper_semilattice) and linorder.
    1.29 +* Theory Int: The representation of numerals has changed.  The infix
    1.30 +operator BIT and the bit datatype with constructors B0 and B1 have
    1.31 +disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
    1.32 +place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems
    1.33 +involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"
    1.34 +accordingly.
    1.35 +
    1.36 +* Theory Nat: definition of <= and < on natural numbers no longer
    1.37 +depend on well-founded relations.  INCOMPATIBILITY.  Definitions
    1.38 +le_def and less_def have disappeared.  Consider lemmas not_less
    1.39 +[symmetric, where ?'a = nat] and less_eq [symmetric] instead.
    1.40 +
    1.41 +* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
    1.42 +(whose purpose mainly is for various fold_set functionals) have been
    1.43 +abandoned in favour of the existing algebraic classes
    1.44 +ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
    1.45 +lower_semilattice (resp. upper_semilattice) and linorder.
    1.46  INCOMPATIBILITY.
    1.47  
    1.48 -* Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
    1.49 -form set-specific version is available as Inductive.lfp_ordinal_induct_set.
    1.50 +* Theory Transitive_Closure: induct and cases rules now declare proper
    1.51 +case_names ("base" and "step").  INCOMPATIBILITY.
    1.52 +
    1.53 +* Theorem Inductive.lfp_ordinal_induct generalized to complete
    1.54 +lattices.  The form set-specific version is available as
    1.55 +Inductive.lfp_ordinal_induct_set.
    1.56  
    1.57  * Theorems "power.simps" renamed to "power_int.simps".
    1.58  
    1.59 -* New class semiring_div provides basic abstract properties of semirings
    1.60 +* Class semiring_div provides basic abstract properties of semirings
    1.61  with division and modulo operations.  Subsumes former class dvd_mod.
    1.62  
    1.63 -* Merged theories IntDef, Numeral and IntArith into unified theory Int.
    1.64 +* Merged theories IntDef, Numeral and IntArith into unified theory
    1.65 +Int.  INCOMPATIBILITY.
    1.66 +
    1.67 +* Theory Library/Code_Index: type "index" now represents natural
    1.68 +numbers rather than integers.  INCOMPATIBILITY.
    1.69 +
    1.70 +* New class "uminus" with operation "uminus" (split of from class
    1.71 +"minus" which now only has operation "minus", binary).
    1.72  INCOMPATIBILITY.
    1.73  
    1.74 -* Theory Library/Code_Index: type "index" now represents natural numbers rather
    1.75 -than integers.  INCOMPATIBILITY.
    1.76 -
    1.77 -* New class "uminus" with operation "uminus" (split of from class "minus"
    1.78 -which now only has operation "minus", binary).  INCOMPATIBILITY.
    1.79 -
    1.80  * New primrec package.  Specification syntax conforms in style to
    1.81 -definition/function/....  No separate induction rule is provided.
    1.82 -The "primrec" command distinguishes old-style and new-style specifications
    1.83 +definition/function/....  No separate induction rule is provided.  The
    1.84 +"primrec" command distinguishes old-style and new-style specifications
    1.85  by syntax.  The former primrec package is now named OldPrimrecPackage.
    1.86  When adjusting theories, beware: constants stemming for new-style
    1.87  primrec specifications have authentic syntax.
    1.88  
    1.89  * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
    1.90  
    1.91 -* Library/ListSpace: new theory of arithmetic vector operations.
    1.92 +* Library/ListVector: new theory of arithmetic vector operations.
    1.93  
    1.94  * Constants "card", "internal_split", "option_map" now with authentic
    1.95  syntax.  INCOMPATIBILITY.
    1.96 @@ -90,7 +96,7 @@
    1.97  Sup_set_def, le_def, less_def, option_map_def now with object
    1.98  equality.  INCOMPATIBILITY.
    1.99  
   1.100 -* New method "induction_scheme" derives user-specified induction rules
   1.101 +* Method "induction_scheme" derives user-specified induction rules
   1.102  from wellfounded induction and completeness of patterns. This factors
   1.103  out some operations that are done internally by the function package
   1.104  and makes them available separately. See "HOL/ex/Induction_Scheme.thy"