diff -r 4aed40ecfb43 -r 27dae626822b 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.