# HG changeset patch
# User haftmann
# Date 1410500295 -7200
# Node ID 44692d31a3994b9781019d15f9de04d132e988b3
# Parent  351810c45a4821a069f59100b04a3dad424bbbf4
NEWS

diff -r 351810c45a48 -r 44692d31a399 NEWS
--- a/NEWS	Thu Sep 11 23:12:32 2014 +0200
+++ b/NEWS	Fri Sep 12 07:38:15 2014 +0200
@@ -23,6 +23,11 @@
 
 *** HOL ***
 
+* Bootstrap of listsum as special case of abstract product over lists.
+Fact rename:
+    listsum_def ~> listsum.eq_foldr
+INCOMPATIBILITY.
+
 * Command and antiquotation "value" provide different evaluation slots (again),
 where the previous strategy (nbe after ML) serves as default.
 Minor INCOMPATIBILITY.