NEWS

--- a/NEWS	Sun Dec 30 10:34:56 2018 +0000
+++ b/NEWS	Sun Dec 30 10:34:56 2018 +0000
@@ -84,7 +84,8 @@
 INCOMPATIBILITY.
 
 * Strong congruence rules (with =simp=> in the premises) for constant f
-are now uniformly called f_cong_strong. 
+are now uniformly called f_cong_simp, in accordance with congruence
+rules produced for mappers by the datatype package. INCOMPATIBILITY.
 
 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
 provers, has been updated.