# HG changeset patch
# User paulson
# Date 931434918 -7200
# Node ID f5c5b81b3f141a68b186ba061f487fda49ae920c
# Parent  78a2ce8fb8dfb647bb056b493ab9404150c5566b
integer division

diff -r 78a2ce8fb8df -r f5c5b81b3f14 NEWS
--- a/NEWS	Thu Jul 08 13:48:11 1999 +0200
+++ b/NEWS	Thu Jul 08 13:55:18 1999 +0200
@@ -7,6 +7,11 @@
 
 *** Overview of INCOMPATIBILITIES (see below for more details) ***
 
+* HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
+are no longer simplified.  (This allows the simplifier to unfold recursive
+functional programs.)  To restore the old behaviour, declare
+	Delcongs [if_weak_cong];
+
 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
 complement;
 
@@ -102,6 +107,11 @@
 nat/int formulae where the two parts interact, such as `m < n ==>
 int(m) < int(n)'.
 
+* Integer division and remainder can now be performed on constant arguments.  
+
+* Many properties of integer multiplication, division and remainder are now
+available.
+
 * New bounded quantifier syntax (input only):
   ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P