NEWS
changeset 69546 27dae626822b
parent 69506 7d59af98af29
child 69569 2d88bf80c84f
     1.1 --- a/NEWS	Sun Dec 30 10:34:56 2018 +0000
     1.2 +++ b/NEWS	Sun Dec 30 10:34:56 2018 +0000
     1.3 @@ -84,7 +84,8 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  * Strong congruence rules (with =simp=> in the premises) for constant f
     1.7 -are now uniformly called f_cong_strong. 
     1.8 +are now uniformly called f_cong_simp, in accordance with congruence
     1.9 +rules produced for mappers by the datatype package. INCOMPATIBILITY.
    1.10  
    1.11  * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
    1.12  provers, has been updated.