--- a/NEWS Thu Mar 12 13:15:36 1998 +0100
+++ b/NEWS Thu Mar 12 13:17:13 1998 +0100
@@ -23,6 +23,8 @@
*** HOL ***
+* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
+
* HOL/Arithmetic: removed 'pred' (predecessor) function;
* Simplifier: