# HG changeset patch
# User paulson
# Date 890063647 -3600
# Node ID bbe14a54deb3107a4c53d50a148e147069e2ebca
# Parent  a5dcd7e4a37d588483202bb2a4c4ca5ef67f01d9
inverse -> converse

diff -r a5dcd7e4a37d -r bbe14a54deb3 NEWS
--- a/NEWS	Mon Mar 16 16:50:50 1998 +0100
+++ b/NEWS	Mon Mar 16 16:54:07 1998 +0100
@@ -25,7 +25,11 @@
 
 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
 
-* HOL/Arithmetic: removed 'pred' (predecessor) function;
+* HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized
+  some theorems about n-1
+
+* HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
+  "inverse"
 
 * Simplifier: