# HG changeset patch
# User nipkow
# Date 1476799484 -7200
# Node ID 72060e61ca9df7652cbea19517484e280a4355f2
# Parent  d7e0123a752b5c95a395e0e248361e0b16a1e6d2
NEWS

diff -r d7e0123a752b -r 72060e61ca9d NEWS
--- a/NEWS	Tue Oct 18 15:57:34 2016 +0200
+++ b/NEWS	Tue Oct 18 16:04:44 2016 +0200
@@ -281,6 +281,8 @@
     mod_1 ~> mod_by_Suc_0
 INCOMPATIBILITY.
 
+* Renamed "setsum" ~> "sum" and "setprod" ~> "prod".
+
 * Dedicated syntax LENGTH('a) for length of types.
 
 * New proof method "argo" using the built-in Argo solver based on SMT