--- 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