| changeset 69164 | 74f1b0f10b2b |
| parent 69155 | 12ff5e476752 |
| child 69183 | 431414500576 |
--- a/NEWS Sun Oct 21 08:19:06 2018 +0200 +++ b/NEWS Sun Oct 21 09:39:09 2018 +0200 @@ -43,6 +43,9 @@ and prod_mset.swap, similarly to sum.swap and prod.swap. INCOMPATIBILITY. +* Strong congruence rules (with =simp=> in the premises) for constant f +are now uniformly called f_cong_strong. + * Sledgehammer: The URL for SystemOnTPTP, which is used by remote provers, has been updated.