author | paulson |
Mon, 16 Mar 1998 16:54:07 +0100 | |
changeset 4747 | bbe14a54deb3 |
parent 4746 | a5dcd7e4a37d |
child 4748 | 2b8ead8e9393 |
--- 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: