# HG changeset patch
# User paulson
# Date 965636712 -7200
# Node ID fa19ffdbe1de1394b81ed17b8d512f74afb75565
# Parent  d17c0b34d5c86c85dd9b5440d52d3627684e48a6
ZF arith

diff -r d17c0b34d5c8 -r fa19ffdbe1de NEWS
--- a/NEWS	Sun Aug 06 15:26:53 2000 +0200
+++ b/NEWS	Mon Aug 07 10:25:12 2000 +0200
@@ -46,6 +46,8 @@
 * HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
   A/r to A//r;
 
+* ZF: new treatment of arithmetic (nat & int) may break some old proofs;
+
 * Isar/Provers: intro/elim/dest attributes: changed
 intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
 should have to change intro!! to intro? only);
@@ -194,14 +196,9 @@
 
 *** HOL ***
 
-* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
-
 * HOL/Algebra: new theory of rings and univariate polynomials, by
 Clemens Ballarin;
 
-* HOL/record: fixed select-update simplification procedure to handle
-extended records as well; admit "r" as field name;
-
 * HOL/ex: new theory Factorization proving the Fundamental Theorem of
 Arithmetic, by Thomas M Rasmussen;
 
@@ -209,8 +206,16 @@
 basically a generalized version of de-Bruijn representation; very
 useful in avoiding lifting of operations;
 
+* HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's
+Theorem, by Thomas M Rasmussen;
+
+* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
+
 * HOL/Real: "rabs" replaced by overloaded "abs" function;
 
+* HOL/record: fixed select-update simplification procedure to handle
+extended records as well; admit "r" as field name;
+
 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
 other numeric types and also as the identity of groups, rings, etc.;
 
@@ -262,6 +267,20 @@
 case of overlap with user translations (e.g. judgements over tuples);
 
 
+*** ZF ***
+
+* simplification automatically cancels common terms in arithmetic expressions over nat;
+
+* new treatment of nat to minimize type-checking: all operators coerce their 
+operands to a natural number using the function natify, making the algebraic
+laws unconditional;
+
+* as above, for int;
+
+* the integer library now contains many of the usual laws for the orderings, 
+including $<=; 
+
+
 *** FOL & ZF ***
 
 * AddIffs now available, giving theorems of the form P<->Q to the