1.1 --- a/NEWS	Sun Aug 06 15:26:53 2000 +0200
     1.2 +++ b/NEWS	Mon Aug 07 10:25:12 2000 +0200
     1.3 @@ -46,6 +46,8 @@
     1.4  * HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
     1.5    A/r to A//r;
     1.6  
     1.7 +* ZF: new treatment of arithmetic (nat & int) may break some old proofs;
     1.8 +
     1.9  * Isar/Provers: intro/elim/dest attributes: changed
    1.10  intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
    1.11  should have to change intro!! to intro? only);
    1.12 @@ -194,14 +196,9 @@
    1.13  
    1.14  *** HOL ***
    1.15  
    1.16 -* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
    1.17 -
    1.18  * HOL/Algebra: new theory of rings and univariate polynomials, by
    1.19  Clemens Ballarin;
    1.20  
    1.21 -* HOL/record: fixed select-update simplification procedure to handle
    1.22 -extended records as well; admit "r" as field name;
    1.23 -
    1.24  * HOL/ex: new theory Factorization proving the Fundamental Theorem of
    1.25  Arithmetic, by Thomas M Rasmussen;
    1.26  
    1.27 @@ -209,8 +206,16 @@
    1.28  basically a generalized version of de-Bruijn representation; very
    1.29  useful in avoiding lifting of operations;
    1.30  
    1.31 +* HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's
    1.32 +Theorem, by Thomas M Rasmussen;
    1.33 +
    1.34 +* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
    1.35 +
    1.36  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.37  
    1.38 +* HOL/record: fixed select-update simplification procedure to handle
    1.39 +extended records as well; admit "r" as field name;
    1.40 +
    1.41  * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
    1.42  other numeric types and also as the identity of groups, rings, etc.;
    1.43  
    1.44 @@ -262,6 +267,20 @@
    1.45  case of overlap with user translations (e.g. judgements over tuples);
    1.46  
    1.47  
    1.48 +*** ZF ***
    1.49 +
    1.50 +* simplification automatically cancels common terms in arithmetic expressions over nat;
    1.51 +
    1.52 +* new treatment of nat to minimize type-checking: all operators coerce their 
    1.53 +operands to a natural number using the function natify, making the algebraic
    1.54 +laws unconditional;
    1.55 +
    1.56 +* as above, for int;
    1.57 +
    1.58 +* the integer library now contains many of the usual laws for the orderings, 
    1.59 +including $<=; 
    1.60 +
    1.61 +
    1.62  *** FOL & ZF ***
    1.63  
    1.64  * AddIffs now available, giving theorems of the form P<->Q to the