tuned;

--- a/NEWS	Fri Sep 23 10:26:07 2005 +0200
+++ b/NEWS	Fri Sep 23 13:20:47 2005 +0200
@@ -225,7 +225,7 @@
 or ==>.  More generally, erule now works even if the major premise of
 the elimination rule contains !! or ==>.
 
-* Method "rules" has been renamed to "iprover"
+* Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY.
 
 * Reorganized bootstrapping of the Pure theories; CPure is now derived
 from Pure, which contains all common declarations already.  Both