# HG changeset patch
# User nipkow
# Date 881236202 -3600
# Node ID c77a484e4f950546760d30d7ed345a45e7525799
# Parent  40e5c97e988d575d81593316a91e0564b66b4d19
pred -> -1

diff -r 40e5c97e988d -r c77a484e4f95 NEWS
--- a/NEWS	Thu Dec 04 12:44:37 1997 +0100
+++ b/NEWS	Thu Dec 04 12:50:02 1997 +0100
@@ -155,9 +155,13 @@
 
   it be used with the new `split_asm_tac'.
 
-* HOL/Nat: users are strongly encouraged to write "0 < n" rather than
-  "n ~= 0". Theorems and proof tools have been modified towards this
-  `standard'.
+* HOL/Arithmetic:
+  - `pred n' is automatically converted to `n-1'.
+    Users are strongly encouraged not to use `pred' any longer,
+    because it will disappear altogether at some point.
+  - Users are strongly encouraged to write "0 < n" rather than
+    "n ~= 0". Theorems and proof tools have been modified towards this
+    `standard'.
 
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);