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